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  3683  soeq1  5567  solin  5573  soinxp  5720  ordtri3or  6364  isosolem  7322  sorpssi  7705  dfwe2  7750  f1oweALT  7951  soxp  8108  frxp3  8130  xpord3inddlem  8133  elfiun  9381  sornom  10230  ltsopr  10985  elz  12531  dyaddisj  25497  istrkgl  28385  istrkgld  28386  axtgupdim2  28398  tgdim01  28434  tglngval  28478  tgellng  28480  colcom  28485  colrot1  28486  legso  28526  lncom  28549  lnrot1  28550  lnrot2  28551  ttgval  28802  colinearalg  28837  axlowdim2  28887  axlowdim  28888  elntg  28911  elntg2  28912  nb3grprlem2  29308  frgrwopreg  30252  constrsuc  33728  constrcbvlem  33745  istrkg2d  34657  axtgupdim2ALTV  34659  brcolinear2  36046  colineardim1  36049  colinearperm1  36050  fin2so  37601  uneqsn  44014  3orbi123  44501  gpgov  48033  gpgiedgdmel  48040  gpgedgel  48041  gpgedgvtx0  48052  gpgedgvtx1  48053  gpgedgiov  48056  gpgedg2ov  48057  gpgedg2iv  48058  gpg3kgrtriexlem6  48079  gpgprismgr4cycllem3  48087  gpgprismgr4cycllem10  48094  pgnbgreunbgrlem1  48103  pgnbgreunbgrlem4  48109  pgnbgreunbgrlem5  48113