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  523  nbior  941  pm5.55  975  rb-ax2  1819  rb-ax3  1820  rb-ax4  1821  spimfw  2036  hba1w  2117  hba1wOLD  2118  hbe1a  2163  sp  2192  axc4  2269  exmoeu  2632  moanim  2659  moexex  2671  necon1bi  2952  fvrn0  6369  nfunsn  6378  mpt2xneldm  7499  mpt2xopxnop0  7502  ixpprc  8087  fineqv  8332  unbndrank  8870  pf1rcl  19907  stri  29417  hstri  29425  ddemeas  30600  hbntg  32008  bj-modalb  33004  hba1-o  34678  axc5c711  34699  naecoms-o  34708  axc5c4c711  39096  hbntal  39263
  Copyright terms: Public domain W3C validator