Theorem orbi12d 929

Description: Deduction joining two equivalences to form equivalence of disjunctions. (Contributed by NM, 21-Jun-1993.)

Hypotheses

Ref	Expression
bi12d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
bi12d.2	⊢ (𝜑 → (𝜃 ↔ 𝜏))

Assertion

Ref	Expression
orbi12d	⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜏)))

Proof of Theorem orbi12d

Step	Hyp	Ref	Expression
1		bi12d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	orbi1d 927	. 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜃)))
3		bi12d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	3	orbi2d 926	. 2 ⊢ (𝜑 → ((𝜒 ∨ 𝜃) ↔ (𝜒 ∨ 𝜏)))
5	2, 4	bitrd 281	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜏)))

Syntax hints:   → wi 4   ↔ wb 208   ∨ wo 858

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 209  df-or 859

This theorem is referenced by:  pm4.39  989  ifpbi123d  1089  3orbi123d  1455  cadbi123d  1629  eueq3  3672  sbcor  3792  unjust  3906  elun  4104  elprg  4602  eltpg  4642  el7g  4646  reuprg0  4658  rabsnifsb  4678  rabrsn  4680  preq12bg  4808  uniprg  4878  disji2  5081  disjprg  5093  disjxun  5095  axprg  5391  swopolem  5561  sotrieq  5582  isso2i  5588  dmopab2rex  5889  somin1  6115  ordequn  6445  fununi  6590  unima  6936  unpreima  7038  eqfunresadj  7338  ordsucun  7799  funcnvuni  7907  fiunlem  7917  frxp  8099  xporderlem  8100  poxp  8101  fnwelem  8104  fnse  8106  xpord2lem  8115  poxp2  8116  xpord3lem  8122  poxp3  8123  soseq  8132  oacan  8510  omword  8532  oeword  8553  oeoa  8560  qsdisj  8769  wemapso2lem  9493  brwdom  9508  cantnflem1  9637  r0weon  9961  infxpen  9963  sornom  10227  fin1ai  10243  isfin5  10249  isfin6  10250  sdom2en01  10252  enfin2i  10271  enfin1ai  10334  isfin5-2  10341  fin1a2lem7  10356  fin1a2lem11  10360  fin1a2lem13  10362  axdc3lem2  10401  engch  10579  eltskg  10701  tsken  10705  ltsonq  10920  addcanpr  10997  ltsosr  11045  axpre-lttri  11116  lemul1  12036  mulge0b  12055  mulle0b  12056  mulsuble0b  12057  nn1m1nn  12224  avgle  12456  nn0sub  12524  elznn0  12576  elz2  12579  nneo  12650  uztric  12856  mul2lt0bi  13094  ltxr  13110  xrrebnd  13164  xmulval  13221  xmulneg1  13265  ixxun  13358  iccsplit  13482  fzsplit2  13547  uzsplit  13594  nelfzo  13663  fzospliti  13690  fzouzsplit  13693  sqeqor  14222  swrdnd  14661  sumeq1  15706  sumeq2w  15709  sumeq2ii  15710  sumeq2sdv  15720  fz1f1o  15727  summo  15734  fsum  15737  prodeq1f  15926  prodeq1  15927  prodeq2w  15930  prodeq2ii  15931  prodeq2sdv  15943  prodmo  15956  fprod  15961  ruclem12  16263  odd2np1lem  16364  dvdsprime  16711  coprm  16736  vdwapun  17000  vdwlem6  17012  vdwlem10  17016  mreexexlemd  17666  mreexexd  17670  istos  18438  tosso  18439  tleile  18441  resstos  18452  tsrlin  18607  tsrss  18611  islring  20576  isdomn  20741  prmirredlem  21511  domnchr  21571  zntoslem  21595  znfld  21599  fctop  23051  cctop  23053  ppttop  23054  pptbas  23055  isufil  23950  ufilss  23952  fixufil  23969  fin1aufil  23979  xpsdsval  24428  nlmmul0or  24730  pmltpclem1  25497  iundisj2  25598  mbfmax  25698  dvne0  26060  fta1glem2  26216  plymul0or  26329  ofmulrt  26330  quotval  26343  plydivlem3  26346  plydivlem4  26347  plydivex  26348  plydivalg  26350  quotlem  26351  aalioulem2  26384  quad2  26891  dcubic2  26896  dcubic  26898  dquartlem1  26903  dquart  26905  quart  26913  leibpilem2  26993  wilthlem1  27119  muval2  27185  perfectlem2  27281  lgslem1  27348  pntpbnd1  27637  leslss  27989  abssor  28326  n0s0suc  28422  n0s0m1  28442  nn1m1nns  28454  elzn0s  28478  elzs2  28479  zsoring  28489  n0seo  28501  zseo  28502  bdayfinbndcbv  28546  bdayfinbndlem1  28547  bdayfinbndlem2  28548  bdayfinbnd  28549  z12zsodd  28562  legtrid  28747  legso  28755  ishlg  28758  lnhl  28771  symquadlem  28845  islmib  28943  isinag  28994  isinagd  28995  inaghl  29001  brbtwn2  29062  axcontlem2  29122  axcontlem4  29124  axcontlem11  29131  edglnl  29300  nb3grprlem2  29538  hashecclwwlkn1  30235  nfrgr2v  30430  h1datom  31741  atss  32505  atom1d  32512  atord  32547  chirred  32554  elimifd  32701  disji2f  32736  disjif2  32740  disjxpin  32747  iundisj2f  32749  disjunsn  32753  brprop  32859  quad3d  32911  fzsplit3  32955  iundisj2fi  32959  f1ocnt  32962  trleile  33109  domnpropd  33421  subrdom  33429  isprmidl  33584  prmidlc  33594  qsidomlem1  33599  qsidomlem2  33600  mxidlmax  33613  rprmval  33672  isrprm  33673  smatrcl  34053  fsumcvg4  34207  erdsze2lem2  35514  satf  35663  satfv1  35673  satfbrsuc  35676  satfrnmapom  35680  satf0op  35687  sat1el2xp  35689  fmlafvel  35695  fmlasuc  35696  fmla1  35697  isfmlasuc  35698  fmlaomn0  35700  fmlasucdisj  35709  satffunlem1lem1  35712  satffunlem1lem2  35713  satffunlem2lem1  35714  dmopab3rexdif  35715  satffunlem2lem2  35716  satfv1fvfmla1  35733  2goelgoanfmla1  35734  satefvfmla1  35735  funpsstri  36076  seglelin  36426  lineunray  36457  prodeq12sdv  36538  cbvsumdavw  36599  cbvproddavw  36600  cbvsumdavw2  36615  cbvproddavw2  36616  weiunval  36782  axtcond  36798  topdifinffinlem  37801  topdifinffin  37802  topdifinfeq  37804  mblfinlem2  38117  itg2addnclem2  38131  iblabsnclem  38142  ftc1anclem5  38156  fdc1  38205  unichnidl  38490  ispridl  38493  maxidlmax  38502  disjressuc2  38870  qsdisjALTV  39158  lcvexchlem4  39621  lcvexchlem5  39622  2at0mat0  40109  pmapjoin  40436  cdlemg17h  41252  dihlspsnat  41917  lzunuz  43309  dvdsrabdioph  43347  acongeq12d  43516  jm2.25  43536  rmydioph  43551  expdioph  43560  fnwe2val  43586  aomclem8  43598  fzunt  43991  fzuntd  43992  fzunt1d  43993  fzuntgd  43994  sqrtcvallem1  44167  brfvrcld2  44228  uneqsn  44561  ntrneixb  44631  ntrneix3  44633  ntrneix13  44635  mnringmulrcld  44764  disjinfi  45730  salexct  46868  salexct2  46873  salexct3  46876  salgencntex  46877  salgensscntex  46878  nnfoctbdjlem  46989  nnfoctbdj  46990  iundjiun  46994  opprb  47585  euoreqb  47663  el1fzopredsuc  47880  iccpartgel  47995  paireqne  48077  divgcdoddALTV  48264  perfectALTVlem2  48304  clnbgrel  48410  dfvopnbgr2  48435  vopnbgrel  48436  dfclnbgr6  48438  dfnbgr6  48439  clnbgrgrim  48516  gpg5nbgrvtx03starlem1  48650  gpg5nbgrvtx03starlem2  48651  gpg5nbgrvtx03starlem3  48652  gpg5nbgrvtx13starlem1  48653  gpg5nbgrvtx13starlem2  48654  gpg5nbgrvtx13starlem3  48655  gpg5edgnedg  48712  lindslinindsimp2lem5  49044  ldepspr  49055  rrx2pnedifcoorneor  49298  rrx2plord  49302  rrx2plordisom  49305  itsclc0yqsol  49346