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 𝜃