Theorem con2d 625

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

This theorem is referenced by:  mt2d  626  con3d  632  pm3.2im  638  con2  644  pm2.65  660  con1biimdc  874  exists2  2139  necon2ad  2421  necon2bd  2422  minel  3508  nlimsucg  4598  poirr2  5058  funun  5298  imadif  5334  infnlbti  7085  mkvprop  7217  addnidpig  7396  zltnle  9363  zdcle  9393  btwnnz  9411  prime  9416  icc0r  9992  fznlem  10107  qltnle  10313  bcval4  10823  seq3coll  10913  fsum3cvg  11521  fsumsplit  11550  fproddccvg  11715  fprodsplitdc  11739  2sqpwodd  12314  pockthg  12495  prmunb  12500  logbgcd1irr  15099  lgsne0  15154