Theorem 3orbi123d 1438

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

Hypotheses

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

Assertion

Ref	Expression
3orbi123d	⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜂) ↔ (𝜒 ∨ 𝜏 ∨ 𝜁)))

Proof of Theorem 3orbi123d

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

Syntax hints:   → wi 4   ↔ wb 196   ∨ wo 382   ∨ w3o 1053

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 197  df-or 384  df-3or 1055

This theorem is referenced by:  moeq3  3416  soeq1  5083  solin  5087  soinxp  5217  ordtri3or  5793  isosolem  6637  sorpssi  6985  dfwe2  7023  f1oweALT  7194  soxp  7335  elfiun  8377  sornom  9137  ltsopr  9892  elz  11417  dyaddisj  23410  istrkgl  25402  istrkgld  25403  axtgupdim2  25415  tgdim01  25447  tglngval  25491  tgellng  25493  colcom  25498  colrot1  25499  legso  25539  lncom  25562  lnrot1  25563  lnrot2  25564  ttgval  25800  colinearalg  25835  axlowdim2  25885  axlowdim  25886  elntg  25909  nb3grprlem2  26327  frgrwopreg  27303  istrkg2d  30872  axtgupdim2OLD  30874  brcolinear2  32290  colineardim1  32293  colinearperm1  32294  fin2so  33526  uneqsn  38638  3orbi123  39034