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

Metamath Proof Explorer

Theorem ecase

Description: Inference for elimination by cases. (Contributed by NM, 13-Jul-2005)

Ref Expression
Hypotheses ecase.1 ⊢ ¬ φ → χ
ecase.2 ⊢ ¬ ψ → χ
ecase.3 ⊢ φ ∧ ψ → χ
Assertion ecase ⊢ χ

Proof

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