andi3or - Mathbox for Richard Penner

	Mathbox for Richard Penner		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > andi3or		Structured version Visualization version Unicode version

Theorem andi3or 38320

Description: Distribute over triple disjunction. (Contributed by RP, 5-Jul-2021.)

**Assertion**
Ref	Expression
andi3or	$/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$

**Proof of Theorem andi3or**
Step	Hyp	Ref	Expression
1		andi 911	. . 3 $/\$ $\/$ $\/$ $/\$ $\/$ $\/$ $/\$
2		andi 911	. . . 4 $/\$ $\/$ $/\$ $\/$ $/\$
3	2	orbi1i 542	. . 3 $/\$ $\/$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
4	1, 3	bitri 264	. 2 $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
5		df-3or 1038	. . 3 $\/$ $\/$ $\/$ $\/$
6	5	anbi2i 730	. 2 $/\$ $\/$ $\/$ $/\$ $\/$ $\/$
7		df-3or 1038	. 2 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
8	4, 6, 7	3bitr4i 292	1 $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$

Colors of variables: wff setvar class

Syntax hints:

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

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 df-3or 1038

This theorem is referenced by: uneqsn 38321