Theorem 3orbi123d 1463

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∨ wo 861   ∨ w3o 1102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862  df-3or 1104

This theorem is used by:  moeq3  3670  soeq1  5580  solin  5586  soinxp  5733  ordtri3or  6395  isosolem  7355  sorpssi  7745  dfwe2  7788  f1oweALT  7984  soxp  8141  frxp3  8168  xpord3inddlem  8171  elfiun  9422  sornom  10355  ltsopr  11117  elz  12695  dyaddisj  25917  istrkgl  28920  istrkgld  28921  axtgupdim2  28933  tgdim01  28970  tglngval  29014  tgellng  29016  colcom  29021  colrot1  29022  legso  29062  lncom  29090  lnrot1  29091  lnrot2  29092  tgplnfn  29253  plngval  29255  isplng  29256  elplng  29258  plngcplem  29263  ttgval  29452  colinearalg  29488  axlowdim2  29538  axlowdim  29539  elntg  29562  elntg2  29563  nb3grprlem2  29962  frgrwopreg  30924  constrsuc  34370  constrcbvlem  34387  istrkg2d  35295  axtgupdim2ALTV  35297  brcolinear2  36823  colineardim1  36826  colinearperm1  36827  fin2so  38530  uneqsn  45024  3orbi123  45493  gpgov  49139  gpgiedgdmel  49146  gpgedgel  49147  gpgedgvtx0  49158  gpgedgvtx1  49159  gpgedgiov  49162  gpgedg2ov  49163  gpgedg2iv  49164  gpg3kgrtriexlem6  49185  gpgprismgr4cycllem3  49194  gpgprismgr4cycllem10  49201  pgnbgreunbgrlem1  49210  pgnbgreunbgrlem4  49216  pgnbgreunbgrlem5  49220  gpg5edgnedg  49227