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

Metamath Proof Explorer

Theorem ecase2d

Description: Deduction for elimination by cases. (Contributed by NM, 21-Apr-1994) (Proof shortened by Wolf Lammen, 19-Sep-2024)

Ref Expression
Hypotheses ecase2d.1 ⊢ φ → ψ
ecase2d.2 ⊢ φ → ¬ ψ ∧ χ
ecase2d.3 ⊢ φ → ¬ ψ ∧ θ
ecase2d.4 ⊢ φ → τ ∨ χ ∨ θ
Assertion ecase2d ⊢ φ → τ

Proof

Step Hyp Ref Expression
1 ecase2d.1 ⊢ φ → ψ
2 ecase2d.2 ⊢ φ → ¬ ψ ∧ χ
3 ecase2d.3 ⊢ φ → ¬ ψ ∧ θ
4 ecase2d.4 ⊢ φ → τ ∨ χ ∨ θ
5 1 2 mpnanrd ⊢ φ → ¬ χ
6 1 3 mpnanrd ⊢ φ → ¬ θ
7 4 ord ⊢ φ → ¬ τ → χ ∨ θ
8 5 6 7 mtord ⊢ φ → ¬ ¬ τ
9 8 notnotrd ⊢ φ → τ