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  2462  necon1ai  2463  fvrn0  5484  nfunsn  5492  ixpprc  6805  fineqv  7046  unbndrank  7482  homarcl  13823  pf1rcl  19395  stri  22798  hstri  22806  hbntg  23532  ax4567  26969  hbntal  27455  hba1wK  28266  ax12o10lem5K  28288  ax12o10lem5X  28289  ax12o10lem7K  28292  ax12o10lem7X  28293  ax12o10lem10K  28297  ax12o10lem10X  28299  nalequcomsX  28351  ax10lem17ALT  28373  ax9lem7  28396  ax9lem9  28398  ax9lem11  28400  ax9lem17  28406
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator