Metamath Proof Explorer


Theorem ecase2dOLD

Description: Obsolete version of ecase2d as of 19-Sep-2024. (Contributed by NM, 21-Apr-1994) (Proof shortened by Wolf Lammen, 22-Dec-2012) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses ecase2d.1 φ ψ
ecase2d.2 φ ¬ ψ χ
ecase2d.3 φ ¬ ψ θ
ecase2d.4 φ τ χ θ
Assertion ecase2dOLD φ τ

Proof

Step Hyp Ref Expression
1 ecase2d.1 φ ψ
2 ecase2d.2 φ ¬ ψ χ
3 ecase2d.3 φ ¬ ψ θ
4 ecase2d.4 φ τ χ θ
5 idd φ τ τ
6 2 pm2.21d φ ψ χ τ
7 1 6 mpand φ χ τ
8 3 pm2.21d φ ψ θ τ
9 1 8 mpand φ θ τ
10 7 9 jaod φ χ θ τ
11 5 10 4 mpjaod φ τ