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

Theorem con1i 142
 Description: A contraposition inference. Inference associated with con1 141. Its associated inference is mt3 190. (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 140 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  144  nsyl4  154  impi  158  simplim  161  pm3.13  520  nbior  900  pm5.55  936  rb-ax2  1668  rb-ax3  1669  rb-ax4  1670  spimfw  1828  hba1w  1923  sp  1990  axc4  1991  exmoeu  2394  moanim  2421  moexex  2433  necon1bi  2714  fvrn0  6015  nfunsn  6024  mpt2xneldm  7105  mpt2xopxnop0  7108  ixpprc  7695  fineqv  7940  unbndrank  8468  pf1rcl  19442  wlkntrllem3  25833  stri  28292  hstri  28300  ddemeas  29426  hbntg  30801  bj-modalb  31731  bj-naecomsv  31773  wl-nf-nf2  32314  wl-axc7ea  32331  wl-dveeq12  32383  hba1-o  33094  axc5c711  33115  naecoms-o  33124  axc5c4c711  37525  hbntal  37691
 Copyright terms: Public domain W3C validator