Theorem orbi12d 919

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 917	. 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜃)))
3		bi12d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	3	orbi2d 916	. 2 ⊢ (𝜑 → ((𝜒 ∨ 𝜃) ↔ (𝜒 ∨ 𝜏)))
5	2, 4	bitrd 279	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜏)))

Syntax hints:   → wi 4   ↔ wb 206   ∨ wo 848

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

This theorem is referenced by:  pm4.39  979  ifpbi123d  1079  3orbi123d  1437  cadbi123d  1610  eueq3  3717  sbcor  3839  unjust  3955  elun  4153  elprg  4648  eltpg  4686  el7g  4690  reuprg0  4702  rabsnifsb  4722  rabrsn  4724  preq12bg  4853  uniprg  4923  disji2  5127  disjprg  5139  disjxun  5141  swopolem  5602  sotrieq  5623  isso2i  5629  dmopab2rex  5928  somin1  6153  ordequn  6487  fununi  6641  unima  6984  unpreima  7083  eqfunresadj  7380  ordsucun  7845  funcnvuni  7954  fiunlem  7966  frxp  8151  xporderlem  8152  poxp  8153  fnwelem  8156  fnse  8158  xpord2lem  8167  poxp2  8168  xpord3lem  8174  poxp3  8175  soseq  8184  oacan  8586  omword  8608  oeword  8628  oeoa  8635  qsdisj  8834  wemapso2lem  9592  brwdom  9607  cantnflem1  9729  r0weon  10052  infxpen  10054  sornom  10317  fin1ai  10333  isfin5  10339  isfin6  10340  sdom2en01  10342  enfin2i  10361  enfin1ai  10424  isfin5-2  10431  fin1a2lem7  10446  fin1a2lem11  10450  fin1a2lem13  10452  axdc3lem2  10491  engch  10668  eltskg  10790  tsken  10794  ltsonq  11009  addcanpr  11086  ltsosr  11134  axpre-lttri  11205  lemul1  12119  mulge0b  12138  mulle0b  12139  mulsuble0b  12140  nn1m1nn  12287  avgle  12508  nn0sub  12576  elznn0  12628  elz2  12631  nneo  12702  uztric  12902  mul2lt0bi  13141  ltxr  13157  xrrebnd  13210  xmulval  13267  xmulneg1  13311  ixxun  13403  iccsplit  13525  fzsplit2  13589  uzsplit  13636  nelfzo  13704  fzospliti  13731  fzouzsplit  13734  sqeqor  14255  swrdnd  14692  sumeq1  15725  sumeq2w  15728  sumeq2ii  15729  sumeq2sdv  15739  fz1f1o  15746  summo  15753  fsum  15756  prodeq1f  15942  prodeq1  15943  prodeq2w  15946  prodeq2ii  15947  prodeq2sdv  15959  prodmo  15972  fprod  15977  ruclem12  16277  odd2np1lem  16377  dvdsprime  16724  coprm  16748  vdwapun  17012  vdwlem6  17024  vdwlem10  17028  mreexexlemd  17687  mreexexd  17691  istos  18463  tosso  18464  tleile  18466  tsrlin  18630  tsrss  18634  islring  20540  isdomn  20705  prmirredlem  21483  domnchr  21547  zntoslem  21575  znfld  21579  fctop  23011  cctop  23013  ppttop  23014  pptbas  23015  isufil  23911  ufilss  23913  fixufil  23930  fin1aufil  23940  xpsdsval  24391  nlmmul0or  24704  pmltpclem1  25483  iundisj2  25584  mbfmax  25684  dvne0  26050  fta1glem2  26208  plymul0or  26322  ofmulrt  26323  quotval  26334  plydivlem3  26337  plydivlem4  26338  plydivex  26339  plydivalg  26341  quotlem  26342  aalioulem2  26375  quad2  26882  dcubic2  26887  dcubic  26889  dquartlem1  26894  dquart  26896  quart  26904  leibpilem2  26984  wilthlem1  27111  muval2  27177  perfectlem2  27274  lgslem1  27341  pntpbnd1  27630  slelss  27946  abssor  28270  n0s0suc  28345  n0s0m1  28359  elzn0s  28384  elzs2  28385  n0seo  28405  zseo  28406  legtrid  28599  legso  28607  ishlg  28610  lnhl  28623  symquadlem  28697  islmib  28795  isinag  28846  isinagd  28847  inaghl  28853  brbtwn2  28920  axcontlem2  28980  axcontlem4  28982  axcontlem11  28989  edglnl  29160  nb3grprlem2  29398  hashecclwwlkn1  30096  nfrgr2v  30291  h1datom  31601  atss  32365  atom1d  32372  atord  32407  chirred  32414  elimifd  32556  disji2f  32590  disjif2  32594  disjxpin  32601  iundisj2f  32603  disjunsn  32607  brprop  32706  quad3d  32754  fzsplit3  32795  iundisj2fi  32799  f1ocnt  32804  resstos  32957  trleile  32961  domnpropd  33280  subrdom  33288  isprmidl  33466  prmidlc  33476  qsidomlem1  33480  qsidomlem2  33481  mxidlmax  33493  rprmval  33544  isrprm  33545  smatrcl  33795  fsumcvg4  33949  erdsze2lem2  35209  satf  35358  satfv1  35368  satfbrsuc  35371  satfrnmapom  35375  satf0op  35382  sat1el2xp  35384  fmlafvel  35390  fmlasuc  35391  fmla1  35392  isfmlasuc  35393  fmlaomn0  35395  fmlasucdisj  35404  satffunlem1lem1  35407  satffunlem1lem2  35408  satffunlem2lem1  35409  dmopab3rexdif  35410  satffunlem2lem2  35411  satfv1fvfmla1  35428  2goelgoanfmla1  35429  satefvfmla1  35430  funpsstri  35766  seglelin  36117  lineunray  36148  prodeq12sdv  36219  cbvsumdavw  36280  cbvproddavw  36281  cbvsumdavw2  36296  cbvproddavw2  36297  weiunlem1  36463  topdifinffinlem  37348  topdifinffin  37349  topdifinfeq  37351  mblfinlem2  37665  itg2addnclem2  37679  iblabsnclem  37690  ftc1anclem5  37704  fdc1  37753  unichnidl  38038  ispridl  38041  maxidlmax  38050  disjressuc2  38389  qsdisjALTV  38616  lcvexchlem4  39038  lcvexchlem5  39039  2at0mat0  39527  pmapjoin  39854  cdlemg17h  40670  dihlspsnat  41335  lzunuz  42779  dvdsrabdioph  42821  acongeq12d  42991  jm2.25  43011  rmydioph  43026  expdioph  43035  fnwe2val  43061  aomclem8  43073  fzunt  43468  fzuntd  43469  fzunt1d  43470  fzuntgd  43471  sqrtcvallem1  43644  brfvrcld2  43705  uneqsn  44038  ntrneixb  44108  ntrneix3  44110  ntrneix13  44112  mnringmulrcld  44247  disjinfi  45197  salexct  46349  salexct2  46354  salexct3  46357  salgencntex  46358  salgensscntex  46359  nnfoctbdjlem  46470  nnfoctbdj  46471  iundjiun  46475  opprb  47043  euoreqb  47121  el1fzopredsuc  47337  iccpartgel  47416  paireqne  47498  divgcdoddALTV  47669  perfectALTVlem2  47709  clnbgrel  47815  dfvopnbgr2  47839  vopnbgrel  47840  dfclnbgr6  47842  dfnbgr6  47843  clnbgrgrim  47902  gpg5nbgrvtx03starlem1  48024  gpg5nbgrvtx03starlem2  48025  gpg5nbgrvtx03starlem3  48026  gpg5nbgrvtx13starlem1  48027  gpg5nbgrvtx13starlem2  48028  gpg5nbgrvtx13starlem3  48029  lindslinindsimp2lem5  48379  ldepspr  48390  rrx2pnedifcoorneor  48637  rrx2plord  48641  rrx2plordisom  48644  itsclc0yqsol  48685