Theorem con2d 629

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 620	. . . 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 621	. 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 619  ax-in2 620

This theorem is referenced by:  mt2d  630  con3d  636  pm3.2im  642  con2  648  pm2.65  665  con1biimdc  881  exists2  2177  necon2ad  2460  necon2bd  2461  minel  3558  nlimsucg  4670  poirr2  5136  funun  5378  imadif  5417  infnlbti  7268  mkvprop  7400  addnidpig  7599  zltnle  9569  zdcle  9600  btwnnz  9618  prime  9623  icc0r  10205  fznlem  10321  qltnle  10549  bcval4  11060  seq3coll  11152  swrd0g  11290  fsum3cvg  12002  fsumsplit  12031  fproddccvg  12196  fprodsplitdc  12220  bitsinv1lem  12585  2sqpwodd  12811  pockthg  12993  prmunb  12998  logbgcd1irr  15761  lgsne0  15840  eupth2lem3lem4fi  16397