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 313	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜂) ↔ (𝜒 ∨ 𝜏 ∨ 𝜁)))

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

This theorem is referenced by:  moeq3  3706  soeq1  5615  solin  5619  soinxp  5763  ordtri3or  6408  isosolem  7359  sorpssi  7740  dfwe2  7782  f1oweALT  7986  soxp  8143  frxp3  8165  xpord3inddlem  8168  elfiun  9473  sornom  10320  ltsopr  11075  elz  12612  dyaddisj  25616  istrkgl  28385  istrkgld  28386  axtgupdim2  28398  tgdim01  28434  tglngval  28478  tgellng  28480  colcom  28485  colrot1  28486  legso  28526  lncom  28549  lnrot1  28550  lnrot2  28551  ttgval  28802  ttgvalOLD  28803  colinearalg  28844  axlowdim2  28894  axlowdim  28895  elntg  28918  elntg2  28919  nb3grprlem2  29317  frgrwopreg  30256  constrsuc  33596  istrkg2d  34512  axtgupdim2ALTV  34514  brcolinear2  35882  colineardim1  35885  colinearperm1  35886  fin2so  37308  uneqsn  43692  3orbi123  44187