Theorem 3orbi123d 1463

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∨ wo 861   ∨ w3o 1102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862  df-3or 1104

This theorem is used by:  moeq3  3677  soeq1  5592  solin  5598  soinxp  5745  ordtri3or  6397  isosolem  7354  sorpssi  7736  dfwe2  7779  f1oweALT  7975  soxp  8131  frxp3  8153  xpord3inddlem  8156  elfiun  9397  sornom  10276  ltsopr  11034  elz  12610  dyaddisj  25808  istrkgl  28780  istrkgld  28781  axtgupdim2  28793  tgdim01  28829  tglngval  28873  tgellng  28875  colcom  28880  colrot1  28881  legso  28921  lncom  28948  lnrot1  28949  lnrot2  28950  tgplnfn  29110  plngval  29112  isplng  29113  elplng  29115  plngcplem  29120  ttgval  29281  colinearalg  29317  axlowdim2  29367  axlowdim  29368  elntg  29391  elntg2  29392  nb3grprlem2  29791  frgrwopreg  30747  constrsuc  34194  constrcbvlem  34211  istrkg2d  35120  axtgupdim2ALTV  35122  brcolinear2  36589  colineardim1  36592  colinearperm1  36593  fin2so  38317  uneqsn  44811  3orbi123  45280  gpgov  48867  gpgiedgdmel  48874  gpgedgel  48875  gpgedgvtx0  48886  gpgedgvtx1  48887  gpgedgiov  48890  gpgedg2ov  48891  gpgedg2iv  48892  gpg3kgrtriexlem6  48913  gpgprismgr4cycllem3  48922  gpgprismgr4cycllem10  48929  pgnbgreunbgrlem1  48938  pgnbgreunbgrlem4  48944  pgnbgreunbgrlem5  48948  gpg5edgnedg  48955