Theorem 3orbi123i 1162

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 920	. . 3 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃))
4		bi3.3	. . 3 ⊢ (𝜏 ↔ 𝜂)
5	3, 4	orbi12i 920	. 2 ⊢ (((𝜑 ∨ 𝜒) ∨ 𝜏) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂))
6		df-3or 1093	. 2 ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ ((𝜑 ∨ 𝜒) ∨ 𝜏))
7		df-3or 1093	. 2 ⊢ ((𝜓 ∨ 𝜃 ∨ 𝜂) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂))
8	5, 6, 7	3bitr4i 304	1 ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂))

Syntax hints:   ↔ wb 207   ∨ wo 853   ∨ w3o 1091

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 208  df-or 854  df-3or 1093

This theorem is referenced by:  ne3anior  3029  otthne  5433  brtp  5472  wecmpep  5617  cnvso  6246  sorpss  7678  epweon  7725  epweonALT  7726  soxp  8076  dford2  9539  elfz0lmr  13736  hash3tpde  14453  ltssolem1  27664  axlowdimlem6  29041  elxrge02  33017  constrcbvlem  33946  dfon2  36025  frege129d  44214  dfxlim2  46298  usgrexmpl2trifr  48535