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  5584  solin  5590  soinxp  5737  ordtri3or  6390  isosolem  7349  sorpssi  7731  dfwe2  7774  f1oweALT  7970  soxp  8128  frxp3  8150  xpord3inddlem  8153  elfiun  9403  sornom  10282  ltsopr  11044  elz  12620  dyaddisj  25827  istrkgl  28802  istrkgld  28803  axtgupdim2  28815  tgdim01  28852  tglngval  28896  tgellng  28898  colcom  28903  colrot1  28904  legso  28944  lncom  28972  lnrot1  28973  lnrot2  28974  tgplnfn  29135  plngval  29137  isplng  29138  elplng  29140  plngcplem  29145  ttgval  29334  colinearalg  29370  axlowdim2  29420  axlowdim  29421  elntg  29444  elntg2  29445  nb3grprlem2  29844  frgrwopreg  30806  constrsuc  34251  constrcbvlem  34268  istrkg2d  35177  axtgupdim2ALTV  35179  brcolinear2  36641  colineardim1  36644  colinearperm1  36645  fin2so  38364  uneqsn  44868  3orbi123  45337  gpgov  48961  gpgiedgdmel  48968  gpgedgel  48969  gpgedgvtx0  48980  gpgedgvtx1  48981  gpgedgiov  48984  gpgedg2ov  48985  gpgedg2iv  48986  gpg3kgrtriexlem6  49007  gpgprismgr4cycllem3  49016  gpgprismgr4cycllem10  49023  pgnbgreunbgrlem1  49032  pgnbgreunbgrlem4  49038  pgnbgreunbgrlem5  49042  gpg5edgnedg  49049