Theorem 3orbi123d

Description: Deduction joining 3 equivalences to form equivalence of disjunctions. (Contributed by NM, 20-Apr-1994)

	Ref	Expression
Hypotheses	bi3d.1	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )
	bi3d.2	⊢ ( 𝜑 → ( 𝜃 ↔ 𝜏 ) )
	bi3d.3	⊢ ( 𝜑 → ( 𝜂 ↔ 𝜁 ) )
Assertion	3orbi123d	⊢ ( 𝜑 → ( ( 𝜓 ∨ 𝜃 ∨ 𝜂 ) ↔ ( 𝜒 ∨ 𝜏 ∨ 𝜁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		bi3d.1	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )
2		bi3d.2	⊢ ( 𝜑 → ( 𝜃 ↔ 𝜏 ) )
3		bi3d.3	⊢ ( 𝜑 → ( 𝜂 ↔ 𝜁 ) )
4	1 2	orbi12d	⊢ ( 𝜑 → ( ( 𝜓 ∨ 𝜃 ) ↔ ( 𝜒 ∨ 𝜏 ) ) )
5	4 3	orbi12d	⊢ ( 𝜑 → ( ( ( 𝜓 ∨ 𝜃 ) ∨ 𝜂 ) ↔ ( ( 𝜒 ∨ 𝜏 ) ∨ 𝜁 ) ) )
6		df-3or	⊢ ( ( 𝜓 ∨ 𝜃 ∨ 𝜂 ) ↔ ( ( 𝜓 ∨ 𝜃 ) ∨ 𝜂 ) )
7		df-3or	⊢ ( ( 𝜒 ∨ 𝜏 ∨ 𝜁 ) ↔ ( ( 𝜒 ∨ 𝜏 ) ∨ 𝜁 ) )
8	5 6 7	3bitr4g	⊢ ( 𝜑 → ( ( 𝜓 ∨ 𝜃 ∨ 𝜂 ) ↔ ( 𝜒 ∨ 𝜏 ∨ 𝜁 ) ) )