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  3512  nlimsucg  4602  poirr2  5062  funun  5302  imadif  5338  infnlbti  7092  mkvprop  7224  addnidpig  7403  zltnle  9372  zdcle  9402  btwnnz  9420  prime  9425  icc0r  10001  fznlem  10116  qltnle  10333  bcval4  10844  seq3coll  10934  fsum3cvg  11543  fsumsplit  11572  fproddccvg  11737  fprodsplitdc  11761  2sqpwodd  12344  pockthg  12526  prmunb  12531  logbgcd1irr  15203  lgsne0  15279