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

Metamath Proof Explorer

Theorem pm2.61dan

Description: Elimination of an antecedent. (Contributed by NM, 1-Jan-2005)

Ref Expression
Hypotheses pm2.61dan.1 ⊢ φ ∧ ψ → χ
pm2.61dan.2 ⊢ φ ∧ ¬ ψ → χ
Assertion pm2.61dan ⊢ φ → χ

Proof

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