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  1839  necon3bi  2453  necon1ai  2454  fvrn0  5403  nfunsn  5410  ixpprc  6723  fineqv  6963  unbndrank  7398  homarcl  13704  pf1rcl  19264  stri  22667  hstri  22675  hbntg  23330  ax4567  26767  hbntal  27012  ax10lem17ALT  27812  ax9lem7  27835  ax9lem9  27837  ax9lem11  27839  ax9lem17  27845
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator