Theorem 3orbi123d 1461

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

Syntax hints:   → wi 4   ↔ wb 209   ∨ wo 860   ∨ w3o 1100

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 210  df-or 861  df-3or 1102

This theorem is referenced by:  moeq3  3684  soeq1  5591  solin  5597  soinxp  5744  ordtri3or  6394  isosolem  7346  sorpssi  7727  dfwe2  7773  f1oweALT  7969  soxp  8125  frxp3  8147  xpord3inddlem  8150  elfiun  9390  sornom  10261  ltsopr  11017  elz  12593  dyaddisj  25724  istrkgl  28693  istrkgld  28694  axtgupdim2  28706  tgdim01  28742  tglngval  28786  tgellng  28788  colcom  28793  colrot1  28794  legso  28834  lncom  28857  lnrot1  28858  lnrot2  28859  tgplnfn  29015  plngval  29017  isplng  29018  elplng  29020  plngcplem  29025  ttgval  29165  colinearalg  29201  axlowdim2  29251  axlowdim  29252  elntg  29275  elntg2  29276  nb3grprlem2  29672  frgrwopreg  30615  constrsuc  34073  constrcbvlem  34090  istrkg2d  34998  axtgupdim2ALTV  35000  brcolinear2  36483  colineardim1  36486  colinearperm1  36487  fin2so  38180  uneqsn  44677  3orbi123  45146  gpgov  48730  gpgiedgdmel  48737  gpgedgel  48738  gpgedgvtx0  48749  gpgedgvtx1  48750  gpgedgiov  48753  gpgedg2ov  48754  gpgedg2iv  48755  gpg3kgrtriexlem6  48776  gpgprismgr4cycllem3  48785  gpgprismgr4cycllem10  48792  pgnbgreunbgrlem1  48801  pgnbgreunbgrlem4  48807  pgnbgreunbgrlem5  48811  gpg5edgnedg  48818