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  1629  hba1w  1683  ax5o  1719  hba1  1721  hbimd  1723  hbnt  1726  nfnd  1762  naecoms  1890  hba1-o  2090  ax467  2110  naecoms-o  2119  necon3bi  2489  necon1ai  2490  fvrn0  5552  nfunsn  5560  ixpprc  6839  fineqv  7080  unbndrank  7516  homarcl  13862  pf1rcl  19434  stri  22839  hstri  22847  hbntg  24164  ax4567  27612  mpt2xopxnop0  28092  hbntal  28375  ax10lem17ALT  29196  ax9lem7  29219  ax9lem9  29221  ax9lem11  29223  ax9lem17  29229
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator