Theorem con2d 627

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 618	. . . 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 619	. 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 617  ax-in2 618

This theorem is referenced by:  mt2d  628  con3d  634  pm3.2im  640  con2  646  pm2.65  663  con1biimdc  878  exists2  2175  necon2ad  2457  necon2bd  2458  minel  3554  nlimsucg  4662  poirr2  5127  funun  5368  imadif  5407  infnlbti  7216  mkvprop  7348  addnidpig  7546  zltnle  9515  zdcle  9546  btwnnz  9564  prime  9569  icc0r  10151  fznlem  10266  qltnle  10493  bcval4  11004  seq3coll  11096  swrd0g  11231  fsum3cvg  11929  fsumsplit  11958  fproddccvg  12123  fprodsplitdc  12147  bitsinv1lem  12512  2sqpwodd  12738  pockthg  12920  prmunb  12925  logbgcd1irr  15681  lgsne0  15757