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

Theorem con1i 147
Description: A contraposition inference. Inference associated with con1 146. Its associated inference is mt3 200. (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 141 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  150  nsyl4  158  nsyl5  159  impi  164  simplim  167  nbior  884  pm3.13  991  rb-ax2  1753  rb-ax3  1754  rb-ax4  1755  spimfw  1967  hba1w  2048  hbe1a  2138  sp  2174  axc4  2312  exmoeu  2573  necon1bi  2967  fvrn0  6922  nfunsn  6934  mpoxneldm  8201  mpoxopxnop0  8204  ixpprc  8917  fineqv  9267  unbndrank  9841  pf1rcl  22090  stri  31775  hstri  31783  ddemeas  33530  hbntg  35079  bj-modalb  35899  hba1-o  38072  axc5c711  38093  naecoms-o  38102  axc5c4c711  43464  hbntal  43618
  Copyright terms: Public domain W3C validator