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

Theorem con2d 587
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 578 . . . 4  |-  ( -. 
ch  ->  ( ch  ->  -. 
ps ) )
31, 2syl6 33 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  -.  ps )
) )
43com23 77 . 2  |-  ( ph  ->  ( ch  ->  ( ps  ->  -.  ps )
) )
5 pm2.01 579 . 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 577  ax-in2 578
This theorem is referenced by:  mt2d  588  con3d  594  pm3.2im  599  con2  605  pm2.65  618  con1biimdc  801  exists2  2040  necon2ad  2306  necon2bd  2307  minel  3321  nlimsucg  4337  poirr2  4767  funun  4994  imadif  5030  infnlbti  6534  addnidpig  6658  zltnle  8548  zdcle  8575  btwnnz  8592  prime  8597  icc0r  9095  fznlem  9206  qltnle  9402  bcval4  9846  fisumcvg  10419  2sqpwodd  10779
  Copyright terms: Public domain W3C validator