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 989

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 568	. . . 4 $/\$
2		pm2.24 113	. . . . 5
3	2	adantr 471	. . . 4 $/\$
4	1, 3	jca 539	. . 3 $/\$ $/\$
5		pm2.21 112	. . . . 5
6	5	adantr 471	. . . 4 $/\$
7		pm3.4 568	. . . 4 $/\$
8	6, 7	jca 539	. . 3 $/\$ $/\$
9	4, 8	jaoi 385	. 2 $/\$ $\/$ $/\$ $/\$
10		pm2.27 40	. . . . . 6
11	10	imdistani 701	. . . . 5 $/\$ $/\$
12	11	orcd 398	. . . 4 $/\$ $/\$ $\/$ $/\$
13	12	adantrr 728	. . 3 $/\$ $/\$ $/\$ $\/$ $/\$
14		pm2.27 40	. . . . . 6
15	14	imdistani 701	. . . . 5 $/\$ $/\$
16	15	olcd 399	. . . 4 $/\$ $/\$ $\/$ $/\$
17	16	adantrl 727	. . 3 $/\$ $/\$ $/\$ $\/$ $/\$
18	13, 17	pm2.61ian 804	. 2 $/\$ $/\$ $\/$ $/\$
19	9, 18	impbii 192	1 $/\$ $\/$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $\/$ wo 374 $/\$ wa 375

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 190 df-or 376 df-an 377

This theorem is referenced by: dfifp2 1437 ifval 3932 ifpidg 36181 ifpim123g 36190