ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  con2i Unicode version

Theorem con2i 601
Description: A contraposition inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 28-Nov-2008.) (Proof shortened by Wolf Lammen, 13-Jun-2013.)
Hypothesis
Ref Expression
con2i.a  |-  ( ph  ->  -.  ps )
Assertion
Ref Expression
con2i  |-  ( ps 
->  -.  ph )

Proof of Theorem con2i
StepHypRef Expression
1 con2i.a . 2  |-  ( ph  ->  -.  ps )
2 id 19 . 2  |-  ( ps 
->  ps )
31, 2nsyl3 600 1  |-  ( ps 
->  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 588  ax-in2 589
This theorem is referenced by:  nsyl  602  notnot  603  imanim  662  imnan  664  pm4.53r  725  ioran  726  pm3.1  728  oranim  755  xornbi  1349  exalim  1463  exnalim  1610  festino  2083  calemes  2093  fresison  2095  calemos  2096  fesapo  2097  nner  2289  necon2ai  2339  necon2bi  2340  neneqad  2364  ralexim  2406  rexalim  2407  eueq3dc  2831  elndif  3170  ssddif  3280  unssdif  3281  n0i  3338  preleq  4440  dcextest  4465  dmsn0el  4978  funtpg  5144  ftpg  5572  acexmidlemab  5736  reldmtpos  6118  nntri2  6358  nntri3  6361  nndceq  6363  inffiexmid  6768  ctssdccl  6964  mkvprop  7000  elni2  7090  renfdisj  7792  sup3exmid  8683  fzdisj  9800  sumrbdclem  11113
  Copyright terms: Public domain W3C validator