Theorem 3orbi123d 1434

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

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

This theorem is referenced by:  moeq3  3648  soeq1  5521  solin  5525  soinxp  5665  ordtri3or  6293  isosolem  7212  sorpssi  7574  dfwe2  7616  f1oweALT  7806  soxp  7959  elfiun  9178  sornom  10022  ltsopr  10777  elz  12310  dyaddisj  24749  istrkgl  26808  istrkgld  26809  axtgupdim2  26821  tgdim01  26857  tglngval  26901  tgellng  26903  colcom  26908  colrot1  26909  legso  26949  lncom  26972  lnrot1  26973  lnrot2  26974  ttgval  27225  ttgvalOLD  27226  colinearalg  27267  axlowdim2  27317  axlowdim  27318  elntg  27341  elntg2  27342  nb3grprlem2  27737  frgrwopreg  28674  istrkg2d  32633  axtgupdim2ALTV  32635  xpord3ind  33787  brcolinear2  34347  colineardim1  34350  colinearperm1  34351  fin2so  35751  uneqsn  41593  3orbi123  42091