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

Theorem con2d 589
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 580 . . . 4  |-  ( -. 
ch  ->  ( ch  ->  -. 
ps ) )
31, 2syl6 33 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  -.  ps )
) )
43com23 77 . 2  |-  ( ph  ->  ( ch  ->  ( ps  ->  -.  ps )
) )
5 pm2.01 581 . 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 579  ax-in2 580
This theorem is referenced by:  mt2d  590  con3d  596  pm3.2im  601  con2  607  pm2.65  620  con1biimdc  805  exists2  2045  necon2ad  2312  necon2bd  2313  minel  3341  nlimsucg  4372  poirr2  4811  funun  5044  imadif  5080  infnlbti  6700  addnidpig  6874  zltnle  8766  zdcle  8793  btwnnz  8810  prime  8815  icc0r  9313  fznlem  9424  qltnle  9622  bcval4  10125  iseqcoll  10212  fisumcvg  10730  fsum3cvg  10731  fsumsplit  10764  2sqpwodd  11247
  Copyright terms: Public domain W3C validator