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  3485  nlimsucg  4566  poirr2  5022  funun  5261  imadif  5297  infnlbti  7025  mkvprop  7156  addnidpig  7335  zltnle  9299  zdcle  9329  btwnnz  9347  prime  9352  icc0r  9926  fznlem  10041  qltnle  10246  bcval4  10732  seq3coll  10822  fsum3cvg  11386  fsumsplit  11415  fproddccvg  11580  fprodsplitdc  11604  2sqpwodd  12176  pockthg  12355  prmunb  12360  logbgcd1irr  14388  lgsne0  14442