Theorem con2d 619

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 610	. . . 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 611	. 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 609  ax-in2 610

This theorem is referenced by:  mt2d  620  con3d  626  pm3.2im  632  con2  638  pm2.65  654  con1biimdc  868  exists2  2116  necon2ad  2397  necon2bd  2398  minel  3476  nlimsucg  4550  poirr2  5003  funun  5242  imadif  5278  infnlbti  7003  mkvprop  7134  addnidpig  7298  zltnle  9258  zdcle  9288  btwnnz  9306  prime  9311  icc0r  9883  fznlem  9997  qltnle  10202  bcval4  10686  seq3coll  10777  fsum3cvg  11341  fsumsplit  11370  fproddccvg  11535  fprodsplitdc  11559  2sqpwodd  12130  pockthg  12309  prmunb  12314  logbgcd1irr  13679  lgsne0  13733