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  ax17e  1608  spimfw  1636  hba1w  1693  ax5o  1729  hba1  1731  hbimd  1733  hbnt  1736  nfnd  1772  naecoms  1901  hba1-o  2101  ax467  2121  naecoms-o  2130  necon3bi  2500  necon1ai  2501  fvrn0  5566  nfunsn  5574  ixpprc  6853  fineqv  7094  unbndrank  7530  homarcl  13876  pf1rcl  19448  stri  22853  hstri  22861  hbntg  24233  funpartlem  24552  ax4567  27704  mpt2xopxnop0  28197  wlkntrllem5  28349  hbntal  28618  naecomsNEW7  29591  ax10lem17ALT  29745  ax9lem7  29768  ax9lem9  29770  ax9lem11  29772  ax9lem17  29778
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator