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  2142  necon2ad  2424  necon2bd  2425  minel  3513  nlimsucg  4603  poirr2  5063  funun  5303  imadif  5339  infnlbti  7101  mkvprop  7233  addnidpig  7420  zltnle  9389  zdcle  9419  btwnnz  9437  prime  9442  icc0r  10018  fznlem  10133  qltnle  10350  bcval4  10861  seq3coll  10951  fsum3cvg  11560  fsumsplit  11589  fproddccvg  11754  fprodsplitdc  11778  bitsinv1lem  12143  2sqpwodd  12369  pockthg  12551  prmunb  12556  logbgcd1irr  15287  lgsne0  15363