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  1681  ax5o  1717  hba1  1719  hbimd  1721  hbnt  1724  nfnd  1760  naecoms  1888  hba1-o  2088  ax467  2108  naecoms-o  2117  necon3bi  2487  necon1ai  2488  fvrn0  5550  nfunsn  5558  ixpprc  6837  fineqv  7078  unbndrank  7514  homarcl  13860  pf1rcl  19432  stri  22837  hstri  22845  hbntg  24162  ax4567  27601  mpt2xopxnop0  28081  hbntal  28319  ax10lem17ALT  29123  ax9lem7  29146  ax9lem9  29148  ax9lem11  29150  ax9lem17  29156
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator