This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pm2.65da

Description: Deduction for proof by contradiction. (Contributed by NM, 12-Jun-2014)

Ref Expression
Hypotheses pm2.65da.1 ⊢ φ ∧ ψ → χ
pm2.65da.2 ⊢ φ ∧ ψ → ¬ χ
Assertion pm2.65da ⊢ φ → ¬ ψ

Proof

Step Hyp Ref Expression
1 pm2.65da.1 ⊢ φ ∧ ψ → χ
2 pm2.65da.2 ⊢ φ ∧ ψ → ¬ χ
3 1 ex ⊢ φ → ψ → χ
4 2 ex ⊢ φ → ψ → ¬ χ
5 3 4 pm2.65d ⊢ φ → ¬ ψ