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 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  1524  rb-ax3  1525  rb-ax4  1526  ax17e  1625  spimfw  1653  hba1w  1714  sp  1755  ax5o  1757  hbnt  1783  hba1OLD  1795  nfndOLD  1800  hbimdOLD  1825  naecoms  1998  hba1-o  2184  ax467  2204  naecoms-o  2213  necon3bi  2592  necon1ai  2593  fvrn0  5694  nfunsn  5702  mpt2xopxnop0  6403  ixpprc  7020  fineqv  7261  unbndrank  7702  pf1rcl  19837  wlkntrllem5  21418  stri  23609  hstri  23617  hbntg  25187  ax4567  27271  hbntal  27984  naecomsNEW7  28953
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator