Theorem andi3or

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

	Ref	Expression
Assertion	andi3or	⊢ ( ( 𝜑 ∧ ( 𝜓 ∨ 𝜒 ∨ 𝜃 ) ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜑 ∧ 𝜒 ) ∨ ( 𝜑 ∧ 𝜃 ) ) )

Proof

Step	Hyp	Ref	Expression
1		andi	⊢ ( ( 𝜑 ∧ ( ( 𝜓 ∨ 𝜒 ) ∨ 𝜃 ) ) ↔ ( ( 𝜑 ∧ ( 𝜓 ∨ 𝜒 ) ) ∨ ( 𝜑 ∧ 𝜃 ) ) )
2		andi	⊢ ( ( 𝜑 ∧ ( 𝜓 ∨ 𝜒 ) ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜑 ∧ 𝜒 ) ) )
3	2	orbi1i	⊢ ( ( ( 𝜑 ∧ ( 𝜓 ∨ 𝜒 ) ) ∨ ( 𝜑 ∧ 𝜃 ) ) ↔ ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜑 ∧ 𝜒 ) ) ∨ ( 𝜑 ∧ 𝜃 ) ) )
4	1 3	bitri	⊢ ( ( 𝜑 ∧ ( ( 𝜓 ∨ 𝜒 ) ∨ 𝜃 ) ) ↔ ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜑 ∧ 𝜒 ) ) ∨ ( 𝜑 ∧ 𝜃 ) ) )
5		df-3or	⊢ ( ( 𝜓 ∨ 𝜒 ∨ 𝜃 ) ↔ ( ( 𝜓 ∨ 𝜒 ) ∨ 𝜃 ) )
6	5	anbi2i	⊢ ( ( 𝜑 ∧ ( 𝜓 ∨ 𝜒 ∨ 𝜃 ) ) ↔ ( 𝜑 ∧ ( ( 𝜓 ∨ 𝜒 ) ∨ 𝜃 ) ) )
7		df-3or	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜑 ∧ 𝜒 ) ∨ ( 𝜑 ∧ 𝜃 ) ) ↔ ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜑 ∧ 𝜒 ) ) ∨ ( 𝜑 ∧ 𝜃 ) ) )
8	4 6 7	3bitr4i	⊢ ( ( 𝜑 ∧ ( 𝜓 ∨ 𝜒 ∨ 𝜃 ) ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜑 ∧ 𝜒 ) ∨ ( 𝜑 ∧ 𝜃 ) ) )