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  2150  necon2ad  2432  necon2bd  2433  minel  3521  nlimsucg  4613  poirr2  5074  funun  5314  imadif  5353  infnlbti  7127  mkvprop  7259  addnidpig  7448  zltnle  9417  zdcle  9448  btwnnz  9466  prime  9471  icc0r  10047  fznlem  10162  qltnle  10384  bcval4  10895  seq3coll  10985  fsum3cvg  11660  fsumsplit  11689  fproddccvg  11854  fprodsplitdc  11878  bitsinv1lem  12243  2sqpwodd  12469  pockthg  12651  prmunb  12656  logbgcd1irr  15410  lgsne0  15486