Theorem con2d 107

Description: A contraposition deduction. (Contributed by NM, 19-Aug-1993.)

Hypothesis

Ref	Expression
con2d.1	|- (ph -> (ps -> -. ch))

Assertion

Ref	Expression
con2d	|- (ph -> (ch -> -. ps))

Proof of Theorem con2d

Step	Hyp	Ref	Expression
1		notnot2 104	. . 3 |- (-. -. ps -> ps)
2		con2d.1	. . 3 |- (ph -> (ps -> -. ch))
3	1, 2	syl5 28	. 2 |- (ph -> (-. -. ps -> -. ch))
4	3	con4d 97	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-3 8

This theorem is referenced by:  con2  108  mt2d  109  pm3.2im  137  exists2  2294  necon3ad  2553  necon2bd  2566  necon4ad  2578  spcimegf  2934  spcegf  2936  spcimedv  2939  rspcimedv  2958  minel  3607  tfinltfin  4502  tfinnn  4535  imadif  5172  nchoicelem14  6303