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 206   ∨ wo 846   ∨ 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 207  df-or 847  df-3or 1088

This theorem is referenced by:  moeq3  3734  soeq1  5629  solin  5634  soinxp  5781  ordtri3or  6427  isosolem  7383  sorpssi  7764  dfwe2  7809  f1oweALT  8013  soxp  8170  frxp3  8192  xpord3inddlem  8195  elfiun  9499  sornom  10346  ltsopr  11101  elz  12641  dyaddisj  25650  istrkgl  28484  istrkgld  28485  axtgupdim2  28497  tgdim01  28533  tglngval  28577  tgellng  28579  colcom  28584  colrot1  28585  legso  28625  lncom  28648  lnrot1  28649  lnrot2  28650  ttgval  28901  ttgvalOLD  28902  colinearalg  28943  axlowdim2  28993  axlowdim  28994  elntg  29017  elntg2  29018  nb3grprlem2  29416  frgrwopreg  30355  constrsuc  33728  istrkg2d  34643  axtgupdim2ALTV  34645  brcolinear2  36022  colineardim1  36025  colinearperm1  36026  fin2so  37567  uneqsn  43987  3orbi123  44482