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  3672  soeq1  5548  solin  5554  soinxp  5701  ordtri3or  6339  isosolem  7284  sorpssi  7665  dfwe2  7710  f1oweALT  7907  soxp  8062  frxp3  8084  xpord3inddlem  8087  elfiun  9320  sornom  10171  ltsopr  10926  elz  12473  dyaddisj  25495  istrkgl  28407  istrkgld  28408  axtgupdim2  28420  tgdim01  28456  tglngval  28500  tgellng  28502  colcom  28507  colrot1  28508  legso  28548  lncom  28571  lnrot1  28572  lnrot2  28573  ttgval  28824  colinearalg  28859  axlowdim2  28909  axlowdim  28910  elntg  28933  elntg2  28934  nb3grprlem2  29330  frgrwopreg  30271  constrsuc  33721  constrcbvlem  33738  istrkg2d  34650  axtgupdim2ALTV  34652  brcolinear2  36052  colineardim1  36055  colinearperm1  36056  fin2so  37607  uneqsn  44018  3orbi123  44505  gpgov  48046  gpgiedgdmel  48053  gpgedgel  48054  gpgedgvtx0  48065  gpgedgvtx1  48066  gpgedgiov  48069  gpgedg2ov  48070  gpgedg2iv  48071  gpg3kgrtriexlem6  48092  gpgprismgr4cycllem3  48101  gpgprismgr4cycllem10  48108  pgnbgreunbgrlem1  48117  pgnbgreunbgrlem4  48123  pgnbgreunbgrlem5  48127  gpg5edgnedg  48134