Theorem pm2.65d 117

Description: Deduction rule for proof by contradiction.

Hypotheses

Ref	Expression
pm2.65d.1	|- (ph -> (ps -> ch))
pm2.65d.2	|- (ph -> (ps -> -. ch))

Assertion

Ref	Expression
pm2.65d	|- (ph -> -. ps)

Proof of Theorem pm2.65d

Step	Hyp	Ref	Expression
1		pm2.65 115	. 2 |- ((ps -> ch) -> ((ps -> -. ch) -> -. ps))
2		pm2.65d.1	. 2 |- (ph -> (ps -> ch))
3		pm2.65d.2	. 2 |- (ph -> (ps -> -. ch))
4	1, 2, 3	sylc 62	1 |- (ph -> -. ps)

Syntax hints:  -. wn 1   -> wi 2

This theorem is referenced by:  cardlim 3657

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

metamath.org