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

Theorem con1i 123
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 21 . 2  |-  ( -. 
ps  ->  -.  ps )
2 con1i.a . 2  |-  ( -. 
ph  ->  ps )
31, 2nsyl2 121 1  |-  ( -. 
ps  ->  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6
This theorem is referenced by:  nsyl4  136  pm2.24i  138  impi  142  simplim  145  pm3.13  489  pm5.55  872  rb-ax2  1513  rb-ax3  1514  rb-ax4  1515  ax12o10lem5  1639  ax12o10lem7  1641  ax12o10lem10  1644  nalequcoms  1682  ax5o  1693  hbnt  1717  hba1  1718  nfnd  1726  ax467  1752  nalequcoms-o  1840  necon3bi  2460  necon1ai  2461  fvrn0  5449  nfunsn  5457  ixpprc  6770  fineqv  7011  unbndrank  7447  homarcl  13787  pf1rcl  19359  stri  22762  hstri  22770  hbntg  23496  ax4567  26933  hbntal  27335  hba1wK  28146  ax12o10lem5K  28168  ax12o10lem5X  28169  ax12o10lem7K  28172  ax12o10lem7X  28173  ax12o10lem10K  28177  ax12o10lem10X  28179  nalequcomsX  28231  ax10lem17ALT  28253  ax9lem7  28276  ax9lem9  28278  ax9lem11  28280  ax9lem17  28286
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator