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

Theorem con1i 129
Description: A contraposition inference. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Mel L. 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 22 . 2  |-  ( -. 
ps  ->  -.  ps )
2 con1i.a . 2  |-  ( -. 
ph  ->  ps )
31, 2nsyl2 127 1  |-  ( -. 
ps  ->  ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  nsyl4  142  pm2.24i  144  impi  148  simplim  151  pm3.13  501  pm5.55  892  rb-ax2  1561  rb-ax3  1562  rb-ax4  1563  ax5e  1673  spimfw  1700  hba1w  1754  sp  1796  axc4  1797  hba1-o  2206  axc5c711  2226  naecoms-o  2235  exmoeu  2296  moanim  2337  moexex  2356  necon3biOLD  2678  necon1aiOLD  2680  necon1bi  2681  fvrn0  5813  nfunsn  5822  mpt2xopxnop0  6834  ixpprc  7386  fineqv  7631  unbndrank  8152  pf1rcl  17894  wlkntrllem3  23597  stri  25798  hstri  25806  ddemeas  26788  hbntg  27755  axc5c4c711  29795  hbntal  31564  bj-naecomsv  32555
  Copyright terms: Public domain W3C validator