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  3670  soeq1  5553  solin  5559  soinxp  5706  ordtri3or  6349  isosolem  7293  sorpssi  7674  dfwe2  7719  f1oweALT  7916  soxp  8071  frxp3  8093  xpord3inddlem  8096  elfiun  9333  sornom  10187  ltsopr  10943  elz  12490  dyaddisj  25553  istrkgl  28530  istrkgld  28531  axtgupdim2  28543  tgdim01  28579  tglngval  28623  tgellng  28625  colcom  28630  colrot1  28631  legso  28671  lncom  28694  lnrot1  28695  lnrot2  28696  ttgval  28947  colinearalg  28983  axlowdim2  29033  axlowdim  29034  elntg  29057  elntg2  29058  nb3grprlem2  29454  frgrwopreg  30398  constrsuc  33895  constrcbvlem  33912  istrkg2d  34823  axtgupdim2ALTV  34825  brcolinear2  36252  colineardim1  36255  colinearperm1  36256  fin2so  37808  uneqsn  44276  3orbi123  44762  gpgov  48298  gpgiedgdmel  48305  gpgedgel  48306  gpgedgvtx0  48317  gpgedgvtx1  48318  gpgedgiov  48321  gpgedg2ov  48322  gpgedg2iv  48323  gpg3kgrtriexlem6  48344  gpgprismgr4cycllem3  48353  gpgprismgr4cycllem10  48360  pgnbgreunbgrlem1  48369  pgnbgreunbgrlem4  48375  pgnbgreunbgrlem5  48379  gpg5edgnedg  48386