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  9699  zdcle  9730  btwnnz  9750  prime  9755  icc0r  10344  fznlem  10461  qltnle  10694  bcval4  11211  hashf1  11308  seq3coll  11315  swrd0g  11453  fsum3cvg  12169  fsumsplit  12198  fproddccvg  12363  fprodsplitdc  12387  bitsinv1lem  12752  2sqpwodd  12980  pockthg  13164  prmunb  13169  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemirc  13332  logbgcd1irr  16220  chtqub  16313  lgsne0  16379  eupth2lem3lem4fi  16936