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 314	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  3652  soeq1  5535  solin  5539  soinxp  5679  ordtri3or  6313  isosolem  7250  sorpssi  7614  dfwe2  7656  f1oweALT  7847  soxp  8001  elfiun  9233  sornom  10079  ltsopr  10834  elz  12367  dyaddisj  24805  istrkgl  26864  istrkgld  26865  axtgupdim2  26877  tgdim01  26913  tglngval  26957  tgellng  26959  colcom  26964  colrot1  26965  legso  27005  lncom  27028  lnrot1  27029  lnrot2  27030  ttgval  27281  ttgvalOLD  27282  colinearalg  27323  axlowdim2  27373  axlowdim  27374  elntg  27397  elntg2  27398  nb3grprlem2  27793  frgrwopreg  28732  istrkg2d  32691  axtgupdim2ALTV  32693  xpord3ind  33845  brcolinear2  34405  colineardim1  34408  colinearperm1  34409  fin2so  35808  uneqsn  41671  3orbi123  42169