Theorem con2d 596

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 587	. . . 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 588	. 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-1 5  ax-2 6  ax-mp 7  ax-in1 586  ax-in2 587

This theorem is referenced by:  mt2d  597  con3d  603  pm3.2im  609  con2  615  pm2.65  631  con1biimdc  839  exists2  2070  necon2ad  2337  necon2bd  2338  minel  3388  nlimsucg  4439  poirr2  4887  funun  5123  imadif  5159  infnlbti  6863  mkvprop  6979  addnidpig  7086  zltnle  8998  zdcle  9025  btwnnz  9043  prime  9048  icc0r  9596  fznlem  9708  qltnle  9910  bcval4  10385  seq3coll  10472  fsum3cvg  11032  fsumsplit  11062  2sqpwodd  11693