Theorem con2d 625

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 616	. . . 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 617	. 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 615  ax-in2 616

This theorem is referenced by:  mt2d  626  con3d  632  pm3.2im  638  con2  644  pm2.65  661  con1biimdc  875  exists2  2152  necon2ad  2434  necon2bd  2435  minel  3526  nlimsucg  4622  poirr2  5084  funun  5324  imadif  5363  infnlbti  7143  mkvprop  7275  addnidpig  7469  zltnle  9438  zdcle  9469  btwnnz  9487  prime  9492  icc0r  10068  fznlem  10183  qltnle  10408  bcval4  10919  seq3coll  11009  swrd0g  11136  fsum3cvg  11764  fsumsplit  11793  fproddccvg  11958  fprodsplitdc  11982  bitsinv1lem  12347  2sqpwodd  12573  pockthg  12755  prmunb  12760  logbgcd1irr  15514  lgsne0  15590