Theorem con2d 629

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

Step	Hyp	Ref	Expression
1		con2d.1	. . . 4 |- ( ph -> ( ps -> -. ch ) )
2		ax-in2 620	. . . 4 |- ( -. ch -> ( ch -> -. ps ) )
3	1, 2	syl6 33	. . 3 |- ( ph -> ( ps -> ( ch -> -. ps ) ) )
4	3	com23 78	. 2 |- ( ph -> ( ch -> ( ps -> -. ps ) ) )
5		pm2.01 621	. 2 |- ( ( ps -> -. ps ) -> -. ps )
6	4, 5	syl6 33	1 |- ( ph -> ( ch -> -. ps ) )

Syntax hints:   -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 619  ax-in2 620

This theorem is referenced by:  mt2d  630  con3d  636  pm3.2im  642  con2  648  pm2.65  665  con1biimdc  881  exists2  2178  necon2ad  2469  necon2bd  2470  minel  3570  nlimsucg  4688  poirr2  5155  funun  5397  imadif  5436  infnlbti  7317  mkvprop  7449  addnidpig  7651  zltnle  9623  zdcle  9654  btwnnz  9672  prime  9677  icc0r  10259  fznlem  10375  qltnle  10603  bcval4  11114  seq3coll  11214  swrd0g  11352  fsum3cvg  12064  fsumsplit  12093  fproddccvg  12258  fprodsplitdc  12282  bitsinv1lem  12647  2sqpwodd  12873  pockthg  13055  prmunb  13060  logbgcd1irr  15832  lgsne0  15911  eupth2lem3lem4fi  16468