Metamath Proof Explorer


Theorem ccase

Description: Inference for combining cases. (Contributed by NM, 29-Jul-1999) (Proof shortened by Wolf Lammen, 6-Jan-2013)

Ref Expression
Hypotheses ccase.1 φψτ
ccase.2 χψτ
ccase.3 φθτ
ccase.4 χθτ
Assertion ccase φχψθτ

Proof

Step Hyp Ref Expression
1 ccase.1 φψτ
2 ccase.2 χψτ
3 ccase.3 φθτ
4 ccase.4 χθτ
5 1 2 jaoian φχψτ
6 3 4 jaoian φχθτ
7 5 6 jaodan φχψθτ