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  5470  nfunsn  5478  ixpprc  6791  fineqv  7032  unbndrank  7468  homarcl  13808  pf1rcl  19380  stri  22783  hstri  22791  hbntg  23517  ax4567  26954  hbntal  27356  hba1wK  28167  ax12o10lem5K  28189  ax12o10lem5X  28190  ax12o10lem7K  28193  ax12o10lem7X  28194  ax12o10lem10K  28198  ax12o10lem10X  28200  nalequcomsX  28252  ax10lem17ALT  28274  ax9lem7  28297  ax9lem9  28299  ax9lem11  28301  ax9lem17  28307
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator