Theorem 3orbi123d 1438

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

Syntax hints:   → wi 4   ↔ wb 206   ∨ wo 848   ∨ w3o 1086

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 849  df-3or 1088

This theorem is referenced by:  moeq3  3672  soeq1  5561  solin  5567  soinxp  5714  ordtri3or  6357  isosolem  7303  sorpssi  7684  dfwe2  7729  f1oweALT  7926  soxp  8081  frxp3  8103  xpord3inddlem  8106  elfiun  9345  sornom  10199  ltsopr  10955  elz  12502  dyaddisj  25565  istrkgl  28542  istrkgld  28543  axtgupdim2  28555  tgdim01  28591  tglngval  28635  tgellng  28637  colcom  28642  colrot1  28643  legso  28683  lncom  28706  lnrot1  28707  lnrot2  28708  ttgval  28959  colinearalg  28995  axlowdim2  29045  axlowdim  29046  elntg  29069  elntg2  29070  nb3grprlem2  29466  frgrwopreg  30410  constrsuc  33916  constrcbvlem  33933  istrkg2d  34844  axtgupdim2ALTV  34846  brcolinear2  36274  colineardim1  36277  colinearperm1  36278  fin2so  37858  uneqsn  44381  3orbi123  44867  gpgov  48402  gpgiedgdmel  48409  gpgedgel  48410  gpgedgvtx0  48421  gpgedgvtx1  48422  gpgedgiov  48425  gpgedg2ov  48426  gpgedg2iv  48427  gpg3kgrtriexlem6  48448  gpgprismgr4cycllem3  48457  gpgprismgr4cycllem10  48464  pgnbgreunbgrlem1  48473  pgnbgreunbgrlem4  48479  pgnbgreunbgrlem5  48483  gpg5edgnedg  48490