cases2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > cases2		Structured version Visualization version Unicode version

Theorem cases2 993

Description: Case disjunction according to the value of

. (Contributed by BJ, 6-Apr-2019.) (Proof shortened by Wolf Lammen, 2-Jan-2020.)

**Assertion**
Ref	Expression
cases2	$/\$ $\/$ $/\$ $/\$

**Proof of Theorem cases2**
Step	Hyp	Ref	Expression
1		pm3.4 584	. . . 4 $/\$
2		pm2.24 121	. . . . 5
3	2	adantr 481	. . . 4 $/\$
4	1, 3	jca 554	. . 3 $/\$ $/\$
5		pm2.21 120	. . . . 5
6	5	adantr 481	. . . 4 $/\$
7		pm3.4 584	. . . 4 $/\$
8	6, 7	jca 554	. . 3 $/\$ $/\$
9	4, 8	jaoi 394	. 2 $/\$ $\/$ $/\$ $/\$
10		pm2.27 42	. . . . . 6
11	10	imdistani 726	. . . . 5 $/\$ $/\$
12	11	orcd 407	. . . 4 $/\$ $/\$ $\/$ $/\$
13	12	adantrr 753	. . 3 $/\$ $/\$ $/\$ $\/$ $/\$
14		pm2.27 42	. . . . . 6
15	14	imdistani 726	. . . . 5 $/\$ $/\$
16	15	olcd 408	. . . 4 $/\$ $/\$ $\/$ $/\$
17	16	adantrl 752	. . 3 $/\$ $/\$ $/\$ $\/$ $/\$
18	13, 17	pm2.61ian 831	. 2 $/\$ $/\$ $\/$ $/\$
19	9, 18	impbii 199	1 $/\$ $\/$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $\/$ wo 383 $/\$ wa 384

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386

This theorem is referenced by: dfbi3 994 dfifp2 1014 ifval 4127 ifpidg 37836 ifpim123g 37845