Theorem 3orbi123d 1433

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 915	. . 3 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜏)))
4		bi3d.3	. . 3 ⊢ (𝜑 → (𝜂 ↔ 𝜁))
5	3, 4	orbi12d 915	. 2 ⊢ (𝜑 → (((𝜓 ∨ 𝜃) ∨ 𝜂) ↔ ((𝜒 ∨ 𝜏) ∨ 𝜁)))
6		df-3or 1086	. 2 ⊢ ((𝜓 ∨ 𝜃 ∨ 𝜂) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂))
7		df-3or 1086	. 2 ⊢ ((𝜒 ∨ 𝜏 ∨ 𝜁) ↔ ((𝜒 ∨ 𝜏) ∨ 𝜁))
8	5, 6, 7	3bitr4g 313	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜂) ↔ (𝜒 ∨ 𝜏 ∨ 𝜁)))

Syntax hints:   → wi 4   ↔ wb 205   ∨ wo 843   ∨ w3o 1084

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 206  df-or 844  df-3or 1086

This theorem is referenced by:  moeq3  3650  soeq1  5523  solin  5527  soinxp  5667  ordtri3or  6295  isosolem  7211  sorpssi  7573  dfwe2  7615  f1oweALT  7801  soxp  7954  elfiun  9150  sornom  10017  ltsopr  10772  elz  12304  dyaddisj  24741  istrkgl  26800  istrkgld  26801  axtgupdim2  26813  tgdim01  26849  tglngval  26893  tgellng  26895  colcom  26900  colrot1  26901  legso  26941  lncom  26964  lnrot1  26965  lnrot2  26966  ttgval  27217  ttgvalOLD  27218  colinearalg  27259  axlowdim2  27309  axlowdim  27310  elntg  27333  elntg2  27334  nb3grprlem2  27729  frgrwopreg  28666  istrkg2d  32625  axtgupdim2ALTV  32627  xpord3ind  33779  brcolinear2  34339  colineardim1  34342  colinearperm1  34343  fin2so  35743  uneqsn  41586  3orbi123  42084