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  3672  soeq1  5548  solin  5554  soinxp  5701  ordtri3or  6339  isosolem  7284  sorpssi  7665  dfwe2  7710  f1oweALT  7907  soxp  8062  frxp3  8084  xpord3inddlem  8087  elfiun  9320  sornom  10171  ltsopr  10926  elz  12473  dyaddisj  25495  istrkgl  28403  istrkgld  28404  axtgupdim2  28416  tgdim01  28452  tglngval  28496  tgellng  28498  colcom  28503  colrot1  28504  legso  28544  lncom  28567  lnrot1  28568  lnrot2  28569  ttgval  28820  colinearalg  28855  axlowdim2  28905  axlowdim  28906  elntg  28929  elntg2  28930  nb3grprlem2  29326  frgrwopreg  30267  constrsuc  33705  constrcbvlem  33722  istrkg2d  34634  axtgupdim2ALTV  34636  brcolinear2  36036  colineardim1  36039  colinearperm1  36040  fin2so  37591  uneqsn  44002  3orbi123  44489  gpgov  48030  gpgiedgdmel  48037  gpgedgel  48038  gpgedgvtx0  48049  gpgedgvtx1  48050  gpgedgiov  48053  gpgedg2ov  48054  gpgedg2iv  48055  gpg3kgrtriexlem6  48076  gpgprismgr4cycllem3  48085  gpgprismgr4cycllem10  48092  pgnbgreunbgrlem1  48101  pgnbgreunbgrlem4  48107  pgnbgreunbgrlem5  48111  gpg5edgnedg  48118