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

Theorem con1i 146
Description: A contraposition inference. Inference associated with con1 145. 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 144 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  147  nsyl4  157  impi  161  simplim  164  nbior  866  pm5.55  925  pm3.13  969  rb-ax2  1826  rb-ax3  1827  rb-ax4  1828  spimfw  2047  hba1w  2131  hba1wOLD  2132  hbe1a  2177  sp  2207  axc4  2294  exmoeu  2651  moanim  2678  moexex  2690  necon1bi  2971  fvrn0  6358  nfunsn  6367  mpt2xneldm  7491  mpt2xopxnop0  7494  ixpprc  8084  fineqv  8332  unbndrank  8870  pf1rcl  19929  stri  29457  hstri  29465  ddemeas  30640  hbntg  32048  bj-modalb  33044  hba1-o  34706  axc5c711  34727  naecoms-o  34736  axc5c4c711  39129  hbntal  39295
  Copyright terms: Public domain W3C validator