Theorem 3orbi123d 1435

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

Syntax hints:   → wi 4   ↔ wb 205   ∨ wo 845   ∨ 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 206  df-or 846  df-3or 1088

This theorem is referenced by:  moeq3  3708  soeq1  5609  solin  5613  soinxp  5757  ordtri3or  6396  isosolem  7346  sorpssi  7721  dfwe2  7763  f1oweALT  7961  soxp  8117  frxp3  8139  xpord3inddlem  8142  elfiun  9427  sornom  10274  ltsopr  11029  elz  12562  dyaddisj  25120  istrkgl  27747  istrkgld  27748  axtgupdim2  27760  tgdim01  27796  tglngval  27840  tgellng  27842  colcom  27847  colrot1  27848  legso  27888  lncom  27911  lnrot1  27912  lnrot2  27913  ttgval  28164  ttgvalOLD  28165  colinearalg  28206  axlowdim2  28256  axlowdim  28257  elntg  28280  elntg2  28281  nb3grprlem2  28676  frgrwopreg  29614  istrkg2d  33747  axtgupdim2ALTV  33749  brcolinear2  35099  colineardim1  35102  colinearperm1  35103  fin2so  36561  uneqsn  42858  3orbi123  43354