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  3686  soeq1  5570  solin  5576  soinxp  5723  ordtri3or  6367  isosolem  7325  sorpssi  7708  dfwe2  7753  f1oweALT  7954  soxp  8111  frxp3  8133  xpord3inddlem  8136  elfiun  9388  sornom  10237  ltsopr  10992  elz  12538  dyaddisj  25504  istrkgl  28392  istrkgld  28393  axtgupdim2  28405  tgdim01  28441  tglngval  28485  tgellng  28487  colcom  28492  colrot1  28493  legso  28533  lncom  28556  lnrot1  28557  lnrot2  28558  ttgval  28809  colinearalg  28844  axlowdim2  28894  axlowdim  28895  elntg  28918  elntg2  28919  nb3grprlem2  29315  frgrwopreg  30259  constrsuc  33735  constrcbvlem  33752  istrkg2d  34664  axtgupdim2ALTV  34666  brcolinear2  36053  colineardim1  36056  colinearperm1  36057  fin2so  37608  uneqsn  44021  3orbi123  44508  gpgov  48037  gpgiedgdmel  48044  gpgedgel  48045  gpgedgvtx0  48056  gpgedgvtx1  48057  gpgedgiov  48060  gpgedg2ov  48061  gpgedg2iv  48062  gpg3kgrtriexlem6  48083  gpgprismgr4cycllem3  48091  gpgprismgr4cycllem10  48098  pgnbgreunbgrlem1  48107  pgnbgreunbgrlem4  48113  pgnbgreunbgrlem5  48117