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

Theorem con1i 121
Description: A contraposition inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 28-Nov-2008.) (Proof shortened by Wolf Lammen, 19-Jun-2013.)
Hypothesis
Ref Expression
con1i.a  |-  ( -. 
ph  ->  ps )
Assertion
Ref Expression
con1i  |-  ( -. 
ps  ->  ph )

Proof of Theorem con1i
StepHypRef Expression
1 id 19 . 2  |-  ( -. 
ps  ->  -.  ps )
2 con1i.a . 2  |-  ( -. 
ph  ->  ps )
31, 2nsyl2 119 1  |-  ( -. 
ps  ->  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  nsyl4  134  pm2.24i  136  impi  140  simplim  143  pm3.13  487  pm5.55  867  rb-ax2  1508  rb-ax3  1509  rb-ax4  1510  spimfw  1627  hba1w  1682  ax5o  1719  hba1  1721  hbimd  1723  hbnt  1726  nfnd  1762  nalequcoms  1890  hba1-o  2090  ax467  2110  nalequcoms-o  2119  necon3bi  2488  necon1ai  2489  fvrn0  5512  nfunsn  5520  ixpprc  6833  fineqv  7074  unbndrank  7510  homarcl  13856  pf1rcl  19428  stri  22833  hstri  22841  hbntg  23566  ax4567  27012  hbntal  27602  ax10lem17ALT  28402  ax9lem7  28425  ax9lem9  28427  ax9lem11  28429  ax9lem17  28435
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator