Theorem 3or6

Description: Analogue of or4 for triple conjunction. (Contributed by Scott Fenton, 16-Mar-2011)

	Ref	Expression
Assertion	3or6	⊢ ( ( ( 𝜑 ∨ 𝜓 ) ∨ ( 𝜒 ∨ 𝜃 ) ∨ ( 𝜏 ∨ 𝜂 ) ) ↔ ( ( 𝜑 ∨ 𝜒 ∨ 𝜏 ) ∨ ( 𝜓 ∨ 𝜃 ∨ 𝜂 ) ) )

Proof

Step	Hyp	Ref	Expression
1		or4	⊢ ( ( ( ( 𝜑 ∨ 𝜒 ) ∨ 𝜏 ) ∨ ( ( 𝜓 ∨ 𝜃 ) ∨ 𝜂 ) ) ↔ ( ( ( 𝜑 ∨ 𝜒 ) ∨ ( 𝜓 ∨ 𝜃 ) ) ∨ ( 𝜏 ∨ 𝜂 ) ) )
2		or4	⊢ ( ( ( 𝜑 ∨ 𝜒 ) ∨ ( 𝜓 ∨ 𝜃 ) ) ↔ ( ( 𝜑 ∨ 𝜓 ) ∨ ( 𝜒 ∨ 𝜃 ) ) )
3	2	orbi1i	⊢ ( ( ( ( 𝜑 ∨ 𝜒 ) ∨ ( 𝜓 ∨ 𝜃 ) ) ∨ ( 𝜏 ∨ 𝜂 ) ) ↔ ( ( ( 𝜑 ∨ 𝜓 ) ∨ ( 𝜒 ∨ 𝜃 ) ) ∨ ( 𝜏 ∨ 𝜂 ) ) )
4	1 3	bitr2i	⊢ ( ( ( ( 𝜑 ∨ 𝜓 ) ∨ ( 𝜒 ∨ 𝜃 ) ) ∨ ( 𝜏 ∨ 𝜂 ) ) ↔ ( ( ( 𝜑 ∨ 𝜒 ) ∨ 𝜏 ) ∨ ( ( 𝜓 ∨ 𝜃 ) ∨ 𝜂 ) ) )
5		df-3or	⊢ ( ( ( 𝜑 ∨ 𝜓 ) ∨ ( 𝜒 ∨ 𝜃 ) ∨ ( 𝜏 ∨ 𝜂 ) ) ↔ ( ( ( 𝜑 ∨ 𝜓 ) ∨ ( 𝜒 ∨ 𝜃 ) ) ∨ ( 𝜏 ∨ 𝜂 ) ) )
6		df-3or	⊢ ( ( 𝜑 ∨ 𝜒 ∨ 𝜏 ) ↔ ( ( 𝜑 ∨ 𝜒 ) ∨ 𝜏 ) )
7		df-3or	⊢ ( ( 𝜓 ∨ 𝜃 ∨ 𝜂 ) ↔ ( ( 𝜓 ∨ 𝜃 ) ∨ 𝜂 ) )
8	6 7	orbi12i	⊢ ( ( ( 𝜑 ∨ 𝜒 ∨ 𝜏 ) ∨ ( 𝜓 ∨ 𝜃 ∨ 𝜂 ) ) ↔ ( ( ( 𝜑 ∨ 𝜒 ) ∨ 𝜏 ) ∨ ( ( 𝜓 ∨ 𝜃 ) ∨ 𝜂 ) ) )
9	4 5 8	3bitr4i	⊢ ( ( ( 𝜑 ∨ 𝜓 ) ∨ ( 𝜒 ∨ 𝜃 ) ∨ ( 𝜏 ∨ 𝜂 ) ) ↔ ( ( 𝜑 ∨ 𝜒 ∨ 𝜏 ) ∨ ( 𝜓 ∨ 𝜃 ∨ 𝜂 ) ) )