This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( ( 𝜑 ∨ 𝜓 ) ∨ ( 𝜒 ∨ 𝜃 ) ∨ ( 𝜏 ∨ 𝜂 ) ) ↔ ( ( 𝜑 ∨ 𝜒 ∨ 𝜏 ) ∨ ( 𝜓 ∨ 𝜃 ∨ 𝜂 ) ) )