Theorem pm2.65d 117

Description: Deduction rule for proof by contradiction.

Hypotheses

Ref	Expression
pm2.65d.1	⊢ (φ → (ψ → χ))
pm2.65d.2	⊢ (φ → (ψ → ¬ χ))

Assertion

Ref	Expression
pm2.65d	⊢ (φ → ¬ ψ)

Proof of Theorem pm2.65d

Step	Hyp	Ref	Expression
1		pm2.65 115	. 2 ⊢ ((ψ → χ) → ((ψ → ¬ χ) → ¬ ψ))
2		pm2.65d.1	. 2 ⊢ (φ → (ψ → χ))
3		pm2.65d.2	. 2 ⊢ (φ → (ψ → ¬ χ))
4	1, 2, 3	sylc 62	1 ⊢ (φ → ¬ ψ)

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