Theorem 3orbi123d 1434

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  3720  soeq1  5617  solin  5622  soinxp  5769  ordtri3or  6417  isosolem  7366  sorpssi  7747  dfwe2  7792  f1oweALT  7995  soxp  8152  frxp3  8174  xpord3inddlem  8177  elfiun  9467  sornom  10314  ltsopr  11069  elz  12612  dyaddisj  25644  istrkgl  28480  istrkgld  28481  axtgupdim2  28493  tgdim01  28529  tglngval  28573  tgellng  28575  colcom  28580  colrot1  28581  legso  28621  lncom  28644  lnrot1  28645  lnrot2  28646  ttgval  28897  ttgvalOLD  28898  colinearalg  28939  axlowdim2  28989  axlowdim  28990  elntg  29013  elntg2  29014  nb3grprlem2  29412  frgrwopreg  30351  constrsuc  33742  istrkg2d  34659  axtgupdim2ALTV  34661  brcolinear2  36039  colineardim1  36042  colinearperm1  36043  fin2so  37593  uneqsn  44014  3orbi123  44508  gpgov  47936  gpgedgel  47942  gpgedgvtx0  47953  gpgedgvtx1  47954