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  3553  nlimsucg  4658  poirr2  5121  funun  5362  imadif  5401  infnlbti  7204  mkvprop  7336  addnidpig  7534  zltnle  9503  zdcle  9534  btwnnz  9552  prime  9557  icc0r  10134  fznlem  10249  qltnle  10475  bcval4  10986  seq3coll  11077  swrd0g  11207  fsum3cvg  11904  fsumsplit  11933  fproddccvg  12098  fprodsplitdc  12122  bitsinv1lem  12487  2sqpwodd  12713  pockthg  12895  prmunb  12900  logbgcd1irr  15656  lgsne0  15732