Theorem 3orbi123i 1156

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

Syntax hints:   ↔ wb 206   ∨ wo 847   ∨ w3o 1085

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 848  df-3or 1087

This theorem is referenced by:  ne3anior  3020  otthne  5449  brtp  5486  wecmpep  5633  cnvso  6264  sorpss  7707  epweon  7754  epweonALT  7755  soxp  8111  dford2  9580  elfz0lmr  13750  hash3tpde  14465  sltsolem1  27594  axlowdimlem6  28881  elxrge02  32859  constrcbvlem  33752  dfon2  35787  frege129d  43759  dfxlim2  45853  usgrexmpl2trifr  48032