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  7096  mkvprop  7228  addnidpig  7408  zltnle  9377  zdcle  9407  btwnnz  9425  prime  9430  icc0r  10006  fznlem  10121  qltnle  10338  bcval4  10849  seq3coll  10939  fsum3cvg  11548  fsumsplit  11577  fproddccvg  11742  fprodsplitdc  11766  bitsinv1lem  12131  2sqpwodd  12357  pockthg  12539  prmunb  12544  logbgcd1irr  15250  lgsne0  15326