Metamath Proof Explorer


Theorem ecased

Description: Deduction for elimination by cases. (Contributed by NM, 8-Oct-2012)

Ref Expression
Hypotheses ecased.1 ( 𝜑 → ( ¬ 𝜓𝜃 ) )
ecased.2 ( 𝜑 → ( ¬ 𝜒𝜃 ) )
ecased.3 ( 𝜑 → ( ( 𝜓𝜒 ) → 𝜃 ) )
Assertion ecased ( 𝜑𝜃 )

Proof

Step Hyp Ref Expression
1 ecased.1 ( 𝜑 → ( ¬ 𝜓𝜃 ) )
2 ecased.2 ( 𝜑 → ( ¬ 𝜒𝜃 ) )
3 ecased.3 ( 𝜑 → ( ( 𝜓𝜒 ) → 𝜃 ) )
4 pm3.11 ( ¬ ( ¬ 𝜓 ∨ ¬ 𝜒 ) → ( 𝜓𝜒 ) )
5 4 3 syl5 ( 𝜑 → ( ¬ ( ¬ 𝜓 ∨ ¬ 𝜒 ) → 𝜃 ) )
6 1 2 5 ecase3d ( 𝜑𝜃 )