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  3509  nlimsucg  4599  poirr2  5059  funun  5299  imadif  5335  infnlbti  7087  mkvprop  7219  addnidpig  7398  zltnle  9366  zdcle  9396  btwnnz  9414  prime  9419  icc0r  9995  fznlem  10110  qltnle  10316  bcval4  10826  seq3coll  10916  fsum3cvg  11524  fsumsplit  11553  fproddccvg  11718  fprodsplitdc  11742  2sqpwodd  12317  pockthg  12498  prmunb  12503  logbgcd1irr  15140  lgsne0  15195