Theorem con2d 614

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 605	. . . 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 606	. 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 604  ax-in2 605

This theorem is referenced by:  mt2d  615  con3d  621  pm3.2im  627  con2  633  pm2.65  649  con1biimdc  863  exists2  2111  necon2ad  2393  necon2bd  2394  minel  3470  nlimsucg  4543  poirr2  4996  funun  5232  imadif  5268  infnlbti  6991  mkvprop  7122  addnidpig  7277  zltnle  9237  zdcle  9267  btwnnz  9285  prime  9290  icc0r  9862  fznlem  9976  qltnle  10181  bcval4  10665  seq3coll  10755  fsum3cvg  11319  fsumsplit  11348  fproddccvg  11513  fprodsplitdc  11537  2sqpwodd  12108  pockthg  12287  prmunb  12292  logbgcd1irr  13525  lgsne0  13579