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

Syntax hints:   → wi 4   ↔ wb 206   ∨ wo 848   ∨ w3o 1086

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 849  df-3or 1088

This theorem is referenced by:  moeq3  3718  soeq1  5613  solin  5619  soinxp  5767  ordtri3or  6416  isosolem  7367  sorpssi  7749  dfwe2  7794  f1oweALT  7997  soxp  8154  frxp3  8176  xpord3inddlem  8179  elfiun  9470  sornom  10317  ltsopr  11072  elz  12615  dyaddisj  25631  istrkgl  28466  istrkgld  28467  axtgupdim2  28479  tgdim01  28515  tglngval  28559  tgellng  28561  colcom  28566  colrot1  28567  legso  28607  lncom  28630  lnrot1  28631  lnrot2  28632  ttgval  28883  ttgvalOLD  28884  colinearalg  28925  axlowdim2  28975  axlowdim  28976  elntg  28999  elntg2  29000  nb3grprlem2  29398  frgrwopreg  30342  constrsuc  33779  istrkg2d  34681  axtgupdim2ALTV  34683  brcolinear2  36059  colineardim1  36062  colinearperm1  36063  fin2so  37614  uneqsn  44038  3orbi123  44531  gpgov  48001  gpgedgel  48007  gpgedgvtx0  48019  gpgedgvtx1  48020  gpg3kgrtriexlem6  48044