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

Metamath Proof Explorer

Theorem ecase3

Description: Inference for elimination by cases. (Contributed by NM, 23-Mar-1995) (Proof shortened by Wolf Lammen, 26-Nov-2012)

Ref Expression
Hypotheses ecase3.1 ⊢ ( 𝜑 → 𝜒 )
ecase3.2 ⊢ ( 𝜓 → 𝜒 )
ecase3.3 ⊢ ( ¬ ( 𝜑 ∨ 𝜓 ) → 𝜒 )
Assertion ecase3 𝜒

Proof

Step Hyp Ref Expression
1 ecase3.1 ⊢ ( 𝜑 → 𝜒 )
2 ecase3.2 ⊢ ( 𝜓 → 𝜒 )
3 ecase3.3 ⊢ ( ¬ ( 𝜑 ∨ 𝜓 ) → 𝜒 )
4 1 2 jaoi ⊢ ( ( 𝜑 ∨ 𝜓 ) → 𝜒 )
5 4 3 pm2.61i ⊢ 𝜒