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  3672  soeq1  5583  solin  5589  soinxp  5737  ordtri3or  6401  isosolem  7362  sorpssi  7752  dfwe2  7795  f1oweALT  7991  soxp  8151  frxp3  8178  xpord3inddlem  8181  elfiun  9432  sornom  10365  ltsopr  11127  elz  12705  dyaddisj  25929  istrkgl  28932  istrkgld  28933  axtgupdim2  28945  tgdim01  28982  tglngval  29026  tgellng  29028  colcom  29033  colrot1  29034  legso  29074  lncom  29102  lnrot1  29103  lnrot2  29104  tgplnfn  29265  plngval  29267  isplng  29268  elplng  29270  plngcplem  29275  ttgval  29464  colinearalg  29500  axlowdim2  29550  axlowdim  29551  elntg  29574  elntg2  29575  nb3grprlem2  29974  frgrwopreg  30936  constrsuc  34423  constrcbvlem  34440  istrkg2d  35348  axtgupdim2ALTV  35350  brcolinear2  36950  colineardim1  36953  colinearperm1  36954  fin2so  38670  uneqsn  45165  3orbi123  45633  gpgov  49279  gpgiedgdmel  49286  gpgedgel  49287  gpgedgvtx0  49298  gpgedgvtx1  49299  gpgedgiov  49302  gpgedg2ov  49303  gpgedg2iv  49304  gpg3kgrtriexlem6  49325  gpgprismgr4cycllem3  49334  gpgprismgr4cycllem10  49341  pgnbgreunbgrlem1  49350  pgnbgreunbgrlem4  49356  pgnbgreunbgrlem5  49360  gpg5edgnedg  49367