MPE Home 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  1864  hba1w  1960  hba1wOLD  1961  hbe1a  2008  sp  2039  axc4  2113  exmoeu  2489  moanim  2516  moexex  2528  necon1bi  2809  fvrn0  6111  nfunsn  6120  mpt2xneldm  7202  mpt2xopxnop0  7205  ixpprc  7792  fineqv  8037  unbndrank  8565  pf1rcl  19480  wlkntrllem3  25857  stri  28306  hstri  28314  ddemeas  29432  hbntg  30761  bj-modalb  31699  bj-naecomsv  31741  wl-nf-nf2  32266  hba1-o  33003  axc5c711  33024  naecoms-o  33033  axc5c4c711  37427  hbntal  37593
  Copyright terms: Public domain W3C validator