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

Theorem con1i 149
 Description: A contraposition inference. Inference associated with con1 148. Its associated inference is mt3 204. (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 143 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  153  nsyl4  161  nsyl5  162  impi  167  simplim  170  nbior  885  pm3.13  992  rb-ax2  1755  rb-ax3  1756  rb-ax4  1757  spimfw  1969  hba1w  2055  hbe1a  2149  sp  2184  axc4  2342  exmoeu  2667  necon1bi  3042  fvrn0  6691  nfunsn  6700  mpoxneldm  7876  mpoxopxnop0  7879  ixpprc  8481  fineqv  8732  unbndrank  9270  pf1rcl  20982  stri  30049  hstri  30057  ddemeas  31580  hbntg  33135  bj-modalb  34135  hba1-o  36165  axc5c711  36186  naecoms-o  36195  axc5c4c711  41053  hbntal  41207
 Copyright terms: Public domain W3C validator