Theorem 3orbi123d 1437

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

Syntax hints:   → wi 4   ↔ 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:  moeq3  3695  soeq1  5582  solin  5588  soinxp  5736  ordtri3or  6384  isosolem  7340  sorpssi  7723  dfwe2  7768  f1oweALT  7971  soxp  8128  frxp3  8150  xpord3inddlem  8153  elfiun  9442  sornom  10291  ltsopr  11046  elz  12590  dyaddisj  25549  istrkgl  28437  istrkgld  28438  axtgupdim2  28450  tgdim01  28486  tglngval  28530  tgellng  28532  colcom  28537  colrot1  28538  legso  28578  lncom  28601  lnrot1  28602  lnrot2  28603  ttgval  28854  colinearalg  28889  axlowdim2  28939  axlowdim  28940  elntg  28963  elntg2  28964  nb3grprlem2  29360  frgrwopreg  30304  constrsuc  33772  constrcbvlem  33789  istrkg2d  34698  axtgupdim2ALTV  34700  brcolinear2  36076  colineardim1  36079  colinearperm1  36080  fin2so  37631  uneqsn  44049  3orbi123  44536  gpgov  48046  gpgiedgdmel  48053  gpgedgel  48054  gpgedgvtx0  48065  gpgedgvtx1  48066  gpg3kgrtriexlem6  48090  gpgprismgr4cycllem3  48096  gpgprismgr4cycllem10  48103