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 χ