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

Theorem con2i 593
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 592 1  |-  ( ps 
->  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-in1 580  ax-in2 581
This theorem is referenced by:  nsyl  594  notnot  595  imnan  660  ioran  705  pm3.1  707  imanim  824  pm4.53r  843  oranim  846  xornbi  1323  exalim  1437  exnalim  1583  festino  2055  calemes  2065  fresison  2067  calemos  2068  fesapo  2069  nner  2260  necon2ai  2310  necon2bi  2311  neneqad  2335  ralexim  2373  rexalim  2374  eueq3dc  2792  elndif  3127  ssddif  3236  unssdif  3237  n0i  3294  preleq  4386  dcextest  4411  dmsn0el  4915  funtpg  5080  ftpg  5497  acexmidlemab  5662  reldmtpos  6034  nntri2  6271  nntri3  6274  nndceq  6276  inffiexmid  6678  elni2  6936  renfdisj  7609  fzdisj  9529  isumrblem  10828
  Copyright terms: Public domain W3C validator