Theorem con2d 633

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 624	. . . 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 625	. 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 623  ax-in2 624

This theorem is referenced by:  mt2d  634  con3d  640  pm3.2im  646  con2  652  pm2.65  669  con1biimdc  885  exists2  2184  necon2ad  2477  necon2bd  2478  minel  3585  nlimsucg  4708  poirr2  5175  funun  5417  imadif  5456  infnlbti  7356  mkvprop  7488  addnidpig  7693  zltnle  9669  zdcle  9700  btwnnz  9719  prime  9724  icc0r  10307  fznlem  10424  qltnle  10656  bcval4  11168  hashf1  11265  seq3coll  11272  swrd0g  11410  fsum3cvg  12123  fsumsplit  12152  fproddccvg  12317  fprodsplitdc  12341  bitsinv1lem  12706  2sqpwodd  12932  pockthg  13114  prmunb  13119  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilemirc  13253  logbgcd1irr  15992  lgsne0  16071  eupth2lem3lem4fi  16628