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

Syntax hints:   → wi 4   ↔ wb 209   ∨ wo 860   ∨ w3o 1102

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 210  df-or 861  df-3or 1104

This theorem is referenced by:  moeq3  3675  soeq1  5590  solin  5596  soinxp  5743  ordtri3or  6393  isosolem  7345  sorpssi  7726  dfwe2  7769  f1oweALT  7965  soxp  8121  frxp3  8143  xpord3inddlem  8146  elfiun  9386  sornom  10256  ltsopr  11012  elz  12588  dyaddisj  25755  istrkgl  28727  istrkgld  28728  axtgupdim2  28740  tgdim01  28776  tglngval  28820  tgellng  28822  colcom  28827  colrot1  28828  legso  28868  lncom  28895  lnrot1  28896  lnrot2  28897  tgplnfn  29057  plngval  29059  isplng  29060  elplng  29062  plngcplem  29067  ttgval  29224  colinearalg  29260  axlowdim2  29310  axlowdim  29311  elntg  29334  elntg2  29335  nb3grprlem2  29731  frgrwopreg  30674  constrsuc  34128  constrcbvlem  34145  istrkg2d  35053  axtgupdim2ALTV  35055  brcolinear2  36550  colineardim1  36553  colinearperm1  36554  fin2so  38278  uneqsn  44771  3orbi123  45240  gpgov  48827  gpgiedgdmel  48834  gpgedgel  48835  gpgedgvtx0  48846  gpgedgvtx1  48847  gpgedgiov  48850  gpgedg2ov  48851  gpgedg2iv  48852  gpg3kgrtriexlem6  48873  gpgprismgr4cycllem3  48882  gpgprismgr4cycllem10  48889  pgnbgreunbgrlem1  48898  pgnbgreunbgrlem4  48904  pgnbgreunbgrlem5  48908  gpg5edgnedg  48915