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  3668  soeq1  5551  solin  5557  soinxp  5704  ordtri3or  6347  isosolem  7291  sorpssi  7672  dfwe2  7717  f1oweALT  7914  soxp  8069  frxp3  8091  xpord3inddlem  8094  elfiun  9331  sornom  10185  ltsopr  10941  elz  12488  dyaddisj  25551  istrkgl  28479  istrkgld  28480  axtgupdim2  28492  tgdim01  28528  tglngval  28572  tgellng  28574  colcom  28579  colrot1  28580  legso  28620  lncom  28643  lnrot1  28644  lnrot2  28645  ttgval  28896  colinearalg  28932  axlowdim2  28982  axlowdim  28983  elntg  29006  elntg2  29007  nb3grprlem2  29403  frgrwopreg  30347  constrsuc  33844  constrcbvlem  33861  istrkg2d  34772  axtgupdim2ALTV  34774  brcolinear2  36201  colineardim1  36204  colinearperm1  36205  fin2so  37747  uneqsn  44208  3orbi123  44694  gpgov  48230  gpgiedgdmel  48237  gpgedgel  48238  gpgedgvtx0  48249  gpgedgvtx1  48250  gpgedgiov  48253  gpgedg2ov  48254  gpgedg2iv  48255  gpg3kgrtriexlem6  48276  gpgprismgr4cycllem3  48285  gpgprismgr4cycllem10  48292  pgnbgreunbgrlem1  48301  pgnbgreunbgrlem4  48307  pgnbgreunbgrlem5  48311  gpg5edgnedg  48318