Theorem 3orbi123d 1432

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

Syntax hints:   → wi 4   ↔ wb 209   ∨ wo 844   ∨ w3o 1083

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 210  df-or 845  df-3or 1085

This theorem is referenced by:  moeq3  3651  soeq1  5458  solin  5462  soinxp  5597  ordtri3or  6191  isosolem  7079  sorpssi  7435  dfwe2  7476  f1oweALT  7655  soxp  7806  elfiun  8878  sornom  9688  ltsopr  10443  elz  11971  dyaddisj  24200  istrkgl  26252  istrkgld  26253  axtgupdim2  26265  tgdim01  26301  tglngval  26345  tgellng  26347  colcom  26352  colrot1  26353  legso  26393  lncom  26416  lnrot1  26417  lnrot2  26418  ttgval  26669  colinearalg  26704  axlowdim2  26754  axlowdim  26755  elntg  26778  elntg2  26779  nb3grprlem2  27171  frgrwopreg  28108  istrkg2d  32047  axtgupdim2ALTV  32049  brcolinear2  33632  colineardim1  33635  colinearperm1  33636  fin2so  35044  uneqsn  40726  3orbi123  41217