Theorem 3orbi123d 1563

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

Syntax hints:   → wi 4   ↔ wb 198   ∨ wo 878   ∨ w3o 1110

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 199  df-or 879  df-3or 1112

This theorem is referenced by:  moeq3  3608  soeq1  5285  solin  5289  soinxp  5422  ordtri3or  5999  isosolem  6857  sorpssi  7208  dfwe2  7247  f1oweALT  7417  soxp  7559  elfiun  8611  sornom  9421  ltsopr  10176  elz  11713  dyaddisj  23769  istrkgl  25777  istrkgld  25778  axtgupdim2  25790  tgdim01  25826  tglngval  25870  tgellng  25872  colcom  25877  colrot1  25878  legso  25918  lncom  25941  lnrot1  25942  lnrot2  25943  ttgval  26181  colinearalg  26216  axlowdim2  26266  axlowdim  26267  elntg  26290  elntg2  26291  nb3grprlem2  26686  frgrwopreg  27700  istrkg2d  31289  axtgupdim2OLD  31291  brcolinear2  32699  colineardim1  32702  colinearperm1  32703  fin2so  33934  uneqsn  39156  3orbi123  39550