Theorem 3orbi123d 1443

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

Syntax hints:   → wi 4   ↔ wb 207   ∨ wo 853   ∨ w3o 1091

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 208  df-or 854  df-3or 1093

This theorem is referenced by:  moeq3  3653  soeq1  5547  solin  5553  soinxp  5700  ordtri3or  6342  isosolem  7291  sorpssi  7672  dfwe2  7717  f1oweALT  7914  soxp  8069  frxp3  8091  xpord3inddlem  8094  elfiun  9333  sornom  10190  ltsopr  10946  elz  12517  dyaddisj  25581  istrkgl  28544  istrkgld  28545  axtgupdim2  28557  tgdim01  28593  tglngval  28637  tgellng  28639  colcom  28644  colrot1  28645  legso  28685  lncom  28708  lnrot1  28709  lnrot2  28710  ttgval  28961  colinearalg  28997  axlowdim2  29047  axlowdim  29048  elntg  29071  elntg2  29072  nb3grprlem2  29468  frgrwopreg  30411  constrsuc  33922  constrcbvlem  33939  istrkg2d  34850  axtgupdim2ALTV  34852  brcolinear2  36286  colineardim1  36289  colinearperm1  36290  fin2so  37974  uneqsn  44469  3orbi123  44955  gpgov  48533  gpgiedgdmel  48540  gpgedgel  48541  gpgedgvtx0  48552  gpgedgvtx1  48553  gpgedgiov  48556  gpgedg2ov  48557  gpgedg2iv  48558  gpg3kgrtriexlem6  48579  gpgprismgr4cycllem3  48588  gpgprismgr4cycllem10  48595  pgnbgreunbgrlem1  48604  pgnbgreunbgrlem4  48610  pgnbgreunbgrlem5  48614  gpg5edgnedg  48621