Theorem 3orbi123i 1174

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

This proof depends on syntax axioms:   ↔ wb 209   ∨ wo 861   ∨ w3o 1102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862  df-3or 1104

This theorem is used by:  ne3anior  3055  otthne  5473  brtp  5512  wecmpep  5658  cnvso  6296  sorpss  7738  epweon  7783  epweonALT  7784  soxp  8134  dford2  9599  elfz0lmr  13831  hash3tpde  14550  ltssolem1  27876  axlowdimlem6  29334  elxrge02  33288  constrcbvlem  34176  dfon2  36303  frege129d  44530  dfxlim2  46603  usgrexmpl2trifr  48843