Theorem con2d 586

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 577	. . . 4 |- ( -. ch -> ( ch -> -. ps ) )
3	1, 2	syl6 33	. . 3 |- ( ph -> ( ps -> ( ch -> -. ps ) ) )
4	3	com23 77	. 2 |- ( ph -> ( ch -> ( ps -> -. ps ) ) )
5		pm2.01 578	. 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 576  ax-in2 577

This theorem is referenced by:  mt2d  587  con3d  593  pm3.2im  598  con2  604  pm2.65  617  con1biimdc  800  exists2  2038  necon2ad  2302  necon2bd  2303  minel  3305  nlimsucg  4309  poirr2  4737  funun  4964  imadif  4999  infnlbti  6439  addnidpig  6526  zltnle  8397  zdcle  8424  btwnnz  8441  prime  8446  icc0r  8949  fznlem  9060  qltnle  9255  bcval4  9679  2sqpwodd  10554