MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  con1i Structured version   Visualization version   GIF version

Theorem con1i 144
Description: A contraposition inference. Inference associated with con1 143. Its associated inference is mt3 192. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Mel L. O'Cat, 28-Nov-2008.) (Proof shortened by Wolf Lammen, 19-Jun-2013.)
Hypothesis
Ref Expression
con1i.1 𝜑𝜓)
Assertion
Ref Expression
con1i 𝜓𝜑)

Proof of Theorem con1i
StepHypRef Expression
1 id 22 . 2 𝜓 → ¬ 𝜓)
2 con1i.1 . 2 𝜑𝜓)
31, 2nsyl2 142 1 𝜓𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  pm2.24i  146  nsyl4  156  impi  160  simplim  163  pm3.13  522  nbior  904  pm5.55  938  rb-ax2  1675  rb-ax3  1676  rb-ax4  1677  spimfw  1875  hba1w  1971  hba1wOLD  1972  hbe1a  2019  sp  2051  axc4  2126  exmoeu  2501  moanim  2528  moexex  2540  necon1bi  2818  fvrn0  6173  nfunsn  6182  mpt2xneldm  7283  mpt2xopxnop0  7286  ixpprc  7873  fineqv  8119  unbndrank  8649  pf1rcl  19632  stri  28965  hstri  28973  ddemeas  30080  hbntg  31412  bj-modalb  32348  hba1-o  33662  axc5c711  33683  naecoms-o  33692  axc5c4c711  38084  hbntal  38251
  Copyright terms: Public domain W3C validator