Theorem con2d 613

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 604	. . . 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 605	. 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 603  ax-in2 604

This theorem is referenced by:  mt2d  614  con3d  620  pm3.2im  626  con2  632  pm2.65  648  con1biimdc  858  exists2  2096  necon2ad  2365  necon2bd  2366  minel  3424  nlimsucg  4481  poirr2  4931  funun  5167  imadif  5203  infnlbti  6913  mkvprop  7032  addnidpig  7147  zltnle  9103  zdcle  9130  btwnnz  9148  prime  9153  icc0r  9712  fznlem  9824  qltnle  10026  bcval4  10501  seq3coll  10588  fsum3cvg  11150  fsumsplit  11179  fproddccvg  11344  2sqpwodd  11857