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  660  con1biimdc  874  exists2  2150  necon2ad  2432  necon2bd  2433  minel  3521  nlimsucg  4612  poirr2  5072  funun  5312  imadif  5348  infnlbti  7110  mkvprop  7242  addnidpig  7431  zltnle  9400  zdcle  9431  btwnnz  9449  prime  9454  icc0r  10030  fznlem  10145  qltnle  10367  bcval4  10878  seq3coll  10968  fsum3cvg  11608  fsumsplit  11637  fproddccvg  11802  fprodsplitdc  11826  bitsinv1lem  12191  2sqpwodd  12417  pockthg  12599  prmunb  12604  logbgcd1irr  15357  lgsne0  15433