MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  con1i Structured version   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 20 . 2  |-  ( -. 
ps  ->  -.  ps )
2 con1i.a . 2  |-  ( -. 
ph  ->  ps )
31, 2nsyl2 121 1  |-  ( -. 
ps  ->  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  nsyl4  136  pm2.24i  138  impi  142  simplim  145  pm3.13  488  pm5.55  868  rb-ax2  1527  rb-ax3  1528  rb-ax4  1529  ax17e  1628  spimfw  1656  hba1w  1722  sp  1763  ax5o  1765  hbntOLD  1800  hba1OLD  1805  nfndOLD  1810  hbimdOLD  1835  naecoms  2037  hba1-o  2225  ax467  2245  naecoms-o  2254  necon3bi  2639  necon1ai  2640  fvrn0  5745  nfunsn  5753  mpt2xopxnop0  6458  ixpprc  7075  fineqv  7316  unbndrank  7760  pf1rcl  19961  wlkntrllem3  21553  stri  23752  hstri  23760  hbntg  25425  ax4567  27569  hbntal  28577  naecomsNEW7  29556
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator