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  2180  necon2ad  2471  necon2bd  2472  minel  3574  nlimsucg  4693  poirr2  5160  funun  5402  imadif  5441  infnlbti  7330  mkvprop  7462  addnidpig  7667  zltnle  9640  zdcle  9671  btwnnz  9690  prime  9695  icc0r  10278  fznlem  10395  qltnle  10627  bcval4  11139  seq3coll  11239  swrd0g  11377  fsum3cvg  12089  fsumsplit  12118  fproddccvg  12283  fprodsplitdc  12307  bitsinv1lem  12672  2sqpwodd  12898  pockthg  13080  prmunb  13085  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemirc  13219  logbgcd1irr  15958  lgsne0  16037  eupth2lem3lem4fi  16594