Theorem 3orbi123d 1438

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 919	. . 3 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜏)))
4		bi3d.3	. . 3 ⊢ (𝜑 → (𝜂 ↔ 𝜁))
5	3, 4	orbi12d 919	. 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 848   ∨ 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 849  df-3or 1088

This theorem is referenced by:  moeq3  3658  soeq1  5560  solin  5566  soinxp  5713  ordtri3or  6355  isosolem  7302  sorpssi  7683  dfwe2  7728  f1oweALT  7925  soxp  8079  frxp3  8101  xpord3inddlem  8104  elfiun  9343  sornom  10199  ltsopr  10955  elz  12526  dyaddisj  25563  istrkgl  28526  istrkgld  28527  axtgupdim2  28539  tgdim01  28575  tglngval  28619  tgellng  28621  colcom  28626  colrot1  28627  legso  28667  lncom  28690  lnrot1  28691  lnrot2  28692  ttgval  28943  colinearalg  28979  axlowdim2  29029  axlowdim  29030  elntg  29053  elntg2  29054  nb3grprlem2  29450  frgrwopreg  30393  constrsuc  33882  constrcbvlem  33899  istrkg2d  34810  axtgupdim2ALTV  34812  brcolinear2  36240  colineardim1  36243  colinearperm1  36244  fin2so  37928  uneqsn  44452  3orbi123  44938  gpgov  48518  gpgiedgdmel  48525  gpgedgel  48526  gpgedgvtx0  48537  gpgedgvtx1  48538  gpgedgiov  48541  gpgedg2ov  48542  gpgedg2iv  48543  gpg3kgrtriexlem6  48564  gpgprismgr4cycllem3  48573  gpgprismgr4cycllem10  48580  pgnbgreunbgrlem1  48589  pgnbgreunbgrlem4  48595  pgnbgreunbgrlem5  48599  gpg5edgnedg  48606