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 ) )

This proof depends on syntax axioms:   -. wn 3   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 623  ax-in2 624

This theorem is used by:  mt2d  634  con3d  640  pm3.2im  646  con2  652  pm2.65  669  con1biimdc  885  exists2  2184  necon2ad  2477  necon2bd  2478  minel  3586  nlimsucg  4715  poirr2  5183  funun  5425  imadif  5464  infnlbti  7372  mkvprop  7504  addnidpig  7709  zltnle  9701  zdcle  9732  btwnnz  9751  prime  9756  icc0r  10345  fznlem  10462  qltnle  10695  bcval4  11212  hashf1  11309  seq3coll  11316  swrd0g  11454  fsum3cvg  12170  fsumsplit  12199  fproddccvg  12364  fprodsplitdc  12388  bitsinv1lem  12753  2sqpwodd  12981  pockthg  13165  prmunb  13170  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemirc  13333  logbgcd1irr  16203  chtqub  16296  lgsne0  16362  eupth2lem3lem4fi  16919