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

Theorem con2i 567
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 566 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 554  ax-in2 555
This theorem is referenced by:  nsyl  568  notnot  569  imnan  634  ioran  679  pm3.1  681  imanim  796  pm4.53r  815  oranim  818  xornbi  1293  exalim  1407  exnalim  1553  festino  2022  calemes  2032  fresison  2034  calemos  2035  fesapo  2036  nner  2224  necon2ai  2274  necon2bi  2275  neneqad  2299  ralexim  2335  rexalim  2336  eueq3dc  2738  ssnpss  3075  psstr  3077  sspsstr  3078  psssstr  3079  elndif  3096  ssddif  3199  unssdif  3200  n0i  3257  disj4im  3304  preleq  4307  dmsn0el  4818  funtpg  4978  ftpg  5375  acexmidlemab  5534  reldmtpos  5899  nntri2  6104  nntri3  6106  nndceq  6108  elni2  6470  renfdisj  7138  fzdisj  9018
  Copyright terms: Public domain W3C validator