Theorem 3orbi123i 1157

Description: Join 3 biconditionals with disjunction. (Contributed by NM, 17-May-1994.)

Hypotheses

Ref	Expression
bi3.1	⊢ (𝜑 ↔ 𝜓)
bi3.2	⊢ (𝜒 ↔ 𝜃)
bi3.3	⊢ (𝜏 ↔ 𝜂)

Assertion

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

Proof of Theorem 3orbi123i

Step	Hyp	Ref	Expression
1		bi3.1	. . . 4 ⊢ (𝜑 ↔ 𝜓)
2		bi3.2	. . . 4 ⊢ (𝜒 ↔ 𝜃)
3	1, 2	orbi12i 915	. . 3 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃))
4		bi3.3	. . 3 ⊢ (𝜏 ↔ 𝜂)
5	3, 4	orbi12i 915	. 2 ⊢ (((𝜑 ∨ 𝜒) ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂))
6		df-3or 1088	. 2 ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ ((𝜑 ∨ 𝜒) ∨ 𝜏))
7		df-3or 1088	. 2 ⊢ ((𝜓 ∨ 𝜃 ∨ 𝜂) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂))
8	5, 6, 7	3bitr4i 303	1 ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂))

Syntax hints:   ↔ wb 206   ∨ wo 848   ∨ w3o 1086

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 207  df-or 849  df-3or 1088

This theorem is referenced by:  ne3anior  3027  otthne  5435  brtp  5472  wecmpep  5617  cnvso  6247  sorpss  7675  epweon  7722  epweonALT  7723  soxp  8073  dford2  9533  elfz0lmr  13703  hash3tpde  14420  sltsolem1  27647  axlowdimlem6  29003  elxrge02  32994  constrcbvlem  33893  dfon2  35965  frege129d  44040  dfxlim2  46128  usgrexmpl2trifr  48319