Metamath Proof Explorer


Theorem ecase23d

Description: Deduction for elimination by cases. (Contributed by NM, 22-Apr-1994)

Ref Expression
Hypotheses ecase23d.1 φ ¬ χ
ecase23d.2 φ ¬ θ
ecase23d.3 φ ψ χ θ
Assertion ecase23d φ ψ

Proof

Step Hyp Ref Expression
1 ecase23d.1 φ ¬ χ
2 ecase23d.2 φ ¬ θ
3 ecase23d.3 φ ψ χ θ
4 ioran ¬ χ θ ¬ χ ¬ θ
5 1 2 4 sylanbrc φ ¬ χ θ
6 3orass ψ χ θ ψ χ θ
7 3 6 sylib φ ψ χ θ
8 7 ord φ ¬ ψ χ θ
9 5 8 mt3d φ ψ