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

Metamath Proof Explorer

Theorem 3ecase

Description: Inference for elimination by cases. (Contributed by NM, 13-Jul-2005)

Ref Expression
Hypotheses 3ecase.1 ⊢ ( ¬ 𝜑 → 𝜃 )
3ecase.2 ⊢ ( ¬ 𝜓 → 𝜃 )
3ecase.3 ⊢ ( ¬ 𝜒 → 𝜃 )
3ecase.4 ⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → 𝜃 )
Assertion 3ecase 𝜃

Proof

Step Hyp Ref Expression
1 3ecase.1 ⊢ ( ¬ 𝜑 → 𝜃 )
2 3ecase.2 ⊢ ( ¬ 𝜓 → 𝜃 )
3 3ecase.3 ⊢ ( ¬ 𝜒 → 𝜃 )
4 3ecase.4 ⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → 𝜃 )
5 4 3exp ⊢ ( 𝜑 → ( 𝜓 → ( 𝜒 → 𝜃 ) ) )
6 1 2a1d ⊢ ( ¬ 𝜑 → ( 𝜓 → ( 𝜒 → 𝜃 ) ) )
7 5 6 pm2.61i ⊢ ( 𝜓 → ( 𝜒 → 𝜃 ) )
8 7 2 3 pm2.61nii ⊢ 𝜃