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  4657  poirr2  5120  funun  5361  imadif  5400  infnlbti  7189  mkvprop  7321  addnidpig  7519  zltnle  9488  zdcle  9519  btwnnz  9537  prime  9542  icc0r  10118  fznlem  10233  qltnle  10458  bcval4  10969  seq3coll  11059  swrd0g  11187  fsum3cvg  11884  fsumsplit  11913  fproddccvg  12078  fprodsplitdc  12102  bitsinv1lem  12467  2sqpwodd  12693  pockthg  12875  prmunb  12880  logbgcd1irr  15635  lgsne0  15711