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  3666  soeq1  5543  solin  5549  soinxp  5696  ordtri3or  6338  isosolem  7281  sorpssi  7662  dfwe2  7707  f1oweALT  7904  soxp  8059  frxp3  8081  xpord3inddlem  8084  elfiun  9314  sornom  10168  ltsopr  10923  elz  12470  dyaddisj  25524  istrkgl  28436  istrkgld  28437  axtgupdim2  28449  tgdim01  28485  tglngval  28529  tgellng  28531  colcom  28536  colrot1  28537  legso  28577  lncom  28600  lnrot1  28601  lnrot2  28602  ttgval  28853  colinearalg  28888  axlowdim2  28938  axlowdim  28939  elntg  28962  elntg2  28963  nb3grprlem2  29359  frgrwopreg  30303  constrsuc  33751  constrcbvlem  33768  istrkg2d  34679  axtgupdim2ALTV  34681  brcolinear2  36102  colineardim1  36105  colinearperm1  36106  fin2so  37657  uneqsn  44128  3orbi123  44614  gpgov  48152  gpgiedgdmel  48159  gpgedgel  48160  gpgedgvtx0  48171  gpgedgvtx1  48172  gpgedgiov  48175  gpgedg2ov  48176  gpgedg2iv  48177  gpg3kgrtriexlem6  48198  gpgprismgr4cycllem3  48207  gpgprismgr4cycllem10  48214  pgnbgreunbgrlem1  48223  pgnbgreunbgrlem4  48229  pgnbgreunbgrlem5  48233  gpg5edgnedg  48240