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 ( 𝜑𝜏 )