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

Theorem con2d 564
Description: A contraposition deduction. (Contributed by NM, 19-Aug-1993.) (Revised by NM, 12-Feb-2013.)
Hypothesis
Ref Expression
con2d.1  |-  ( ph  ->  ( ps  ->  -.  ch ) )
Assertion
Ref Expression
con2d  |-  ( ph  ->  ( ch  ->  -.  ps ) )

Proof of Theorem con2d
StepHypRef Expression
1 con2d.1 . . . 4  |-  ( ph  ->  ( ps  ->  -.  ch ) )
2 ax-in2 555 . . . 4  |-  ( -. 
ch  ->  ( ch  ->  -. 
ps ) )
31, 2syl6 33 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  -.  ps )
) )
43com23 76 . 2  |-  ( ph  ->  ( ch  ->  ( ps  ->  -.  ps )
) )
5 pm2.01 556 . 2  |-  ( ( ps  ->  -.  ps )  ->  -.  ps )
64, 5syl6 33 1  |-  ( ph  ->  ( ch  ->  -.  ps ) )
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:  mt2d  565  con3d  571  pm3.2im  576  con2  582  pm2.65  595  con1biimdc  778  exists2  2013  necon2ad  2277  necon2bd  2278  minel  3310  nlimsucg  4317  poirr2  4744  funun  4971  imadif  5006  addnidpig  6491  zltnle  8347  zdcle  8374  btwnnz  8391  prime  8395  icc0r  8895  fznlem  9006  qltnle  9202  bcval4  9619
  Copyright terms: Public domain W3C validator