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  880  exists2  2177  necon2ad  2459  necon2bd  2460  minel  3556  nlimsucg  4664  poirr2  5129  funun  5371  imadif  5410  infnlbti  7224  mkvprop  7356  addnidpig  7555  zltnle  9524  zdcle  9555  btwnnz  9573  prime  9578  icc0r  10160  fznlem  10275  qltnle  10502  bcval4  11013  seq3coll  11105  swrd0g  11240  fsum3cvg  11938  fsumsplit  11967  fproddccvg  12132  fprodsplitdc  12156  bitsinv1lem  12521  2sqpwodd  12747  pockthg  12929  prmunb  12934  logbgcd1irr  15690  lgsne0  15766