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  2001  hba1-o  2185  ax467  2205  naecoms-o  2214  necon3bi  2593  necon1ai  2594  fvrn0  5695  nfunsn  5703  mpt2xopxnop0  6404  ixpprc  7021  fineqv  7262  unbndrank  7703  pf1rcl  19838  wlkntrllem5  21419  stri  23610  hstri  23618  hbntg  25188  ax4567  27272  hbntal  27985  naecomsNEW7  28954
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator