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  3659  soeq1  5554  solin  5560  soinxp  5707  ordtri3or  6350  isosolem  7296  sorpssi  7677  dfwe2  7722  f1oweALT  7919  soxp  8073  frxp3  8095  xpord3inddlem  8098  elfiun  9337  sornom  10193  ltsopr  10949  elz  12520  dyaddisj  25576  istrkgl  28543  istrkgld  28544  axtgupdim2  28556  tgdim01  28592  tglngval  28636  tgellng  28638  colcom  28643  colrot1  28644  legso  28684  lncom  28707  lnrot1  28708  lnrot2  28709  ttgval  28960  colinearalg  28996  axlowdim2  29046  axlowdim  29047  elntg  29070  elntg2  29071  nb3grprlem2  29467  frgrwopreg  30411  constrsuc  33901  constrcbvlem  33918  istrkg2d  34829  axtgupdim2ALTV  34831  brcolinear2  36259  colineardim1  36262  colinearperm1  36263  fin2so  37945  uneqsn  44473  3orbi123  44959  gpgov  48533  gpgiedgdmel  48540  gpgedgel  48541  gpgedgvtx0  48552  gpgedgvtx1  48553  gpgedgiov  48556  gpgedg2ov  48557  gpgedg2iv  48558  gpg3kgrtriexlem6  48579  gpgprismgr4cycllem3  48588  gpgprismgr4cycllem10  48595  pgnbgreunbgrlem1  48604  pgnbgreunbgrlem4  48610  pgnbgreunbgrlem5  48614  gpg5edgnedg  48621