cases2 - Metamath Proof Explorer

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

Theorem cases2 980

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 563	. . . 4 $/\$
2		pm2.24 112	. . . . 5
3	2	adantr 466	. . . 4 $/\$
4	1, 3	jca 534	. . 3 $/\$ $/\$
5		pm2.21 111	. . . . 5
6	5	adantr 466	. . . 4 $/\$
7		pm3.4 563	. . . 4 $/\$
8	6, 7	jca 534	. . 3 $/\$ $/\$
9	4, 8	jaoi 380	. 2 $/\$ $\/$ $/\$ $/\$
10		pm2.27 40	. . . . . 6
11	10	imdistani 694	. . . . 5 $/\$ $/\$
12	11	orcd 393	. . . 4 $/\$ $/\$ $\/$ $/\$
13	12	adantrr 721	. . 3 $/\$ $/\$ $/\$ $\/$ $/\$
14		pm2.27 40	. . . . . 6
15	14	imdistani 694	. . . . 5 $/\$ $/\$
16	15	olcd 394	. . . 4 $/\$ $/\$ $\/$ $/\$
17	16	adantrl 720	. . 3 $/\$ $/\$ $/\$ $\/$ $/\$
18	13, 17	pm2.61ian 797	. 2 $/\$ $/\$ $\/$ $/\$
19	9, 18	impbii 190	1 $/\$ $\/$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 187 $\/$ wo 369 $/\$ wa 370

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 188 df-or 371 df-an 372

This theorem is referenced by: dfifp2 1422 ifval 3945 ifpidg 35882 ifpim123g 35891