Theorem con2d 624

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 615	. . . 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 616	. 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 614  ax-in2 615

This theorem is referenced by:  mt2d  625  con3d  631  pm3.2im  637  con2  643  pm2.65  659  con1biimdc  873  exists2  2123  necon2ad  2404  necon2bd  2405  minel  3484  nlimsucg  4565  poirr2  5021  funun  5260  imadif  5296  infnlbti  7024  mkvprop  7155  addnidpig  7334  zltnle  9298  zdcle  9328  btwnnz  9346  prime  9351  icc0r  9925  fznlem  10040  qltnle  10245  bcval4  10731  seq3coll  10821  fsum3cvg  11385  fsumsplit  11414  fproddccvg  11579  fprodsplitdc  11603  2sqpwodd  12175  pockthg  12354  prmunb  12359  logbgcd1irr  14355  lgsne0  14409