Theorem 3orbi123d 1437

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

Syntax hints:   → wi 4   ↔ wb 206   ∨ wo 847   ∨ w3o 1085

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 848  df-3or 1087

This theorem is referenced by:  moeq3  3680  soeq1  5560  solin  5566  soinxp  5713  ordtri3or  6352  isosolem  7304  sorpssi  7685  dfwe2  7730  f1oweALT  7930  soxp  8085  frxp3  8107  xpord3inddlem  8110  elfiun  9357  sornom  10206  ltsopr  10961  elz  12507  dyaddisj  25530  istrkgl  28438  istrkgld  28439  axtgupdim2  28451  tgdim01  28487  tglngval  28531  tgellng  28533  colcom  28538  colrot1  28539  legso  28579  lncom  28602  lnrot1  28603  lnrot2  28604  ttgval  28855  colinearalg  28890  axlowdim2  28940  axlowdim  28941  elntg  28964  elntg2  28965  nb3grprlem2  29361  frgrwopreg  30302  constrsuc  33721  constrcbvlem  33738  istrkg2d  34650  axtgupdim2ALTV  34652  brcolinear2  36039  colineardim1  36042  colinearperm1  36043  fin2so  37594  uneqsn  44007  3orbi123  44494  gpgov  48026  gpgiedgdmel  48033  gpgedgel  48034  gpgedgvtx0  48045  gpgedgvtx1  48046  gpgedgiov  48049  gpgedg2ov  48050  gpgedg2iv  48051  gpg3kgrtriexlem6  48072  gpgprismgr4cycllem3  48080  gpgprismgr4cycllem10  48087  pgnbgreunbgrlem1  48096  pgnbgreunbgrlem4  48102  pgnbgreunbgrlem5  48106