Theorem 3orbi123d 1456

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 929	. . 3 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜏)))
4		bi3d.3	. . 3 ⊢ (𝜑 → (𝜂 ↔ 𝜁))
5	3, 4	orbi12d 929	. 2 ⊢ (𝜑 → (((𝜓 ∨ 𝜃) ∨ 𝜂) ↔ ((𝜒 ∨ 𝜏) ∨ 𝜁)))
6		df-3or 1099	. 2 ⊢ ((𝜓 ∨ 𝜃 ∨ 𝜂) ↔ ((𝜓 ∨ 𝜃) ∨ 𝜂))
7		df-3or 1099	. 2 ⊢ ((𝜒 ∨ 𝜏 ∨ 𝜁) ↔ ((𝜒 ∨ 𝜏) ∨ 𝜁))
8	5, 6, 7	3bitr4g 316	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜂) ↔ (𝜒 ∨ 𝜏 ∨ 𝜁)))

Syntax hints:   → wi 4   ↔ wb 208   ∨ wo 858   ∨ w3o 1097

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 209  df-or 859  df-3or 1099

This theorem is referenced by:  moeq3  3675  soeq1  5576  solin  5582  soinxp  5729  ordtri3or  6378  isosolem  7331  sorpssi  7712  dfwe2  7757  f1oweALT  7953  soxp  8109  frxp3  8131  xpord3inddlem  8134  elfiun  9376  sornom  10234  ltsopr  10990  elz  12570  dyaddisj  25658  istrkgl  28627  istrkgld  28628  axtgupdim2  28640  tgdim01  28676  tglngval  28720  tgellng  28722  colcom  28727  colrot1  28728  legso  28768  lncom  28791  lnrot1  28792  lnrot2  28793  tgplnfn  28982  plngval  28984  isplng  28985  elplng  28987  plngcplem  28992  ttgval  29075  colinearalg  29111  axlowdim2  29161  axlowdim  29162  elntg  29185  elntg2  29186  nb3grprlem2  29582  frgrwopreg  30525  constrsuc  34035  constrcbvlem  34052  istrkg2d  34960  axtgupdim2ALTV  34962  brcolinear2  36408  colineardim1  36411  colinearperm1  36412  fin2so  38106  uneqsn  44601  3orbi123  45087  gpgov  48664  gpgiedgdmel  48671  gpgedgel  48672  gpgedgvtx0  48683  gpgedgvtx1  48684  gpgedgiov  48687  gpgedg2ov  48688  gpgedg2iv  48689  gpg3kgrtriexlem6  48710  gpgprismgr4cycllem3  48719  gpgprismgr4cycllem10  48726  pgnbgreunbgrlem1  48735  pgnbgreunbgrlem4  48741  pgnbgreunbgrlem5  48745  gpg5edgnedg  48752