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  1676  rb-ax3  1677  rb-ax4  1678  spimfw  1876  hba1w  1972  hba1wOLD  1973  hbe1a  2020  sp  2051  axc4  2128  exmoeu  2500  moanim  2527  moexex  2539  necon1bi  2819  fvrn0  6203  nfunsn  6212  mpt2xneldm  7323  mpt2xopxnop0  7326  ixpprc  7914  fineqv  8160  unbndrank  8690  pf1rcl  19694  stri  29086  hstri  29094  ddemeas  30273  hbntg  31685  bj-modalb  32681  hba1-o  34001  axc5c711  34022  naecoms-o  34031  axc5c4c711  38422  hbntal  38589
  Copyright terms: Public domain W3C validator