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  1438  cadbi123d  1612  eueq3  3671  sbcor  3793  unjust  3907  elun  4107  elprg  4605  eltpg  4645  el7g  4649  reuprg0  4661  rabsnifsb  4681  rabrsn  4683  preq12bg  4811  uniprg  4881  disji2  5084  disjprg  5096  disjxun  5098  axprg  5383  swopolem  5550  sotrieq  5571  isso2i  5577  dmopab2rex  5874  somin1  6098  ordequn  6430  fununi  6575  unima  6917  unpreima  7017  eqfunresadj  7316  ordsucun  7777  funcnvuni  7884  fiunlem  7896  frxp  8078  xporderlem  8079  poxp  8080  fnwelem  8083  fnse  8085  xpord2lem  8094  poxp2  8095  xpord3lem  8101  poxp3  8102  soseq  8111  oacan  8485  omword  8507  oeword  8528  oeoa  8535  qsdisj  8743  wemapso2lem  9469  brwdom  9484  cantnflem1  9610  r0weon  9934  infxpen  9936  sornom  10199  fin1ai  10215  isfin5  10221  isfin6  10222  sdom2en01  10224  enfin2i  10243  enfin1ai  10306  isfin5-2  10313  fin1a2lem7  10328  fin1a2lem11  10332  fin1a2lem13  10334  axdc3lem2  10373  engch  10551  eltskg  10673  tsken  10677  ltsonq  10892  addcanpr  10969  ltsosr  11017  axpre-lttri  11088  lemul1  12005  mulge0b  12024  mulle0b  12025  mulsuble0b  12026  nn1m1nn  12178  avgle  12395  nn0sub  12463  elznn0  12515  elz2  12518  nneo  12588  uztric  12787  mul2lt0bi  13025  ltxr  13041  xrrebnd  13095  xmulval  13152  xmulneg1  13196  ixxun  13289  iccsplit  13413  fzsplit2  13477  uzsplit  13524  nelfzo  13592  fzospliti  13619  fzouzsplit  13622  sqeqor  14151  swrdnd  14590  sumeq1  15624  sumeq2w  15627  sumeq2ii  15628  sumeq2sdv  15638  fz1f1o  15645  summo  15652  fsum  15655  prodeq1f  15841  prodeq1  15842  prodeq2w  15845  prodeq2ii  15846  prodeq2sdv  15858  prodmo  15871  fprod  15876  ruclem12  16178  odd2np1lem  16279  dvdsprime  16626  coprm  16650  vdwapun  16914  vdwlem6  16926  vdwlem10  16930  mreexexlemd  17579  mreexexd  17583  istos  18351  tosso  18352  tleile  18354  resstos  18365  tsrlin  18520  tsrss  18524  islring  20485  isdomn  20650  prmirredlem  21439  domnchr  21499  zntoslem  21523  znfld  21527  fctop  22960  cctop  22962  ppttop  22963  pptbas  22964  isufil  23859  ufilss  23861  fixufil  23878  fin1aufil  23888  xpsdsval  24337  nlmmul0or  24639  pmltpclem1  25417  iundisj2  25518  mbfmax  25618  dvne0  25984  fta1glem2  26142  plymul0or  26256  ofmulrt  26257  quotval  26268  plydivlem3  26271  plydivlem4  26272  plydivex  26273  plydivalg  26275  quotlem  26276  aalioulem2  26309  quad2  26817  dcubic2  26822  dcubic  26824  dquartlem1  26829  dquart  26831  quart  26839  leibpilem2  26919  wilthlem1  27046  muval2  27112  perfectlem2  27209  lgslem1  27276  pntpbnd1  27565  leslss  27917  abssor  28254  n0s0suc  28350  n0s0m1  28370  nn1m1nns  28382  elzn0s  28406  elzs2  28407  zsoring  28417  n0seo  28429  zseo  28430  bdayfinbndcbv  28474  bdayfinbndlem1  28475  bdayfinbndlem2  28476  bdayfinbnd  28477  z12zsodd  28490  legtrid  28675  legso  28683  ishlg  28686  lnhl  28699  symquadlem  28773  islmib  28871  isinag  28922  isinagd  28923  inaghl  28929  brbtwn2  28990  axcontlem2  29050  axcontlem4  29052  axcontlem11  29059  edglnl  29228  nb3grprlem2  29466  hashecclwwlkn1  30164  nfrgr2v  30359  h1datom  31669  atss  32433  atom1d  32440  atord  32475  chirred  32482  elimifd  32629  disji2f  32663  disjif2  32667  disjxpin  32674  iundisj2f  32676  disjunsn  32680  brprop  32786  quad3d  32839  fzsplit3  32883  iundisj2fi  32887  f1ocnt  32890  trleile  33063  domnpropd  33370  subrdom  33378  isprmidl  33530  prmidlc  33540  qsidomlem1  33544  qsidomlem2  33545  mxidlmax  33557  rprmval  33608  isrprm  33609  smatrcl  33973  fsumcvg4  34127  erdsze2lem2  35417  satf  35566  satfv1  35576  satfbrsuc  35579  satfrnmapom  35583  satf0op  35590  sat1el2xp  35592  fmlafvel  35598  fmlasuc  35599  fmla1  35600  isfmlasuc  35601  fmlaomn0  35603  fmlasucdisj  35612  satffunlem1lem1  35615  satffunlem1lem2  35616  satffunlem2lem1  35617  dmopab3rexdif  35618  satffunlem2lem2  35619  satfv1fvfmla1  35636  2goelgoanfmla1  35637  satefvfmla1  35638  funpsstri  35979  seglelin  36329  lineunray  36360  prodeq12sdv  36431  cbvsumdavw  36492  cbvproddavw  36493  cbvsumdavw2  36508  cbvproddavw2  36509  weiunval  36675  topdifinffinlem  37599  topdifinffin  37600  topdifinfeq  37602  mblfinlem2  37906  itg2addnclem2  37920  iblabsnclem  37931  ftc1anclem5  37945  fdc1  37994  unichnidl  38279  ispridl  38282  maxidlmax  38291  disjressuc2  38659  qsdisjALTV  38947  lcvexchlem4  39410  lcvexchlem5  39411  2at0mat0  39898  pmapjoin  40225  cdlemg17h  41041  dihlspsnat  41706  lzunuz  43122  dvdsrabdioph  43164  acongeq12d  43333  jm2.25  43353  rmydioph  43368  expdioph  43377  fnwe2val  43403  aomclem8  43415  fzunt  43808  fzuntd  43809  fzunt1d  43810  fzuntgd  43811  sqrtcvallem1  43984  brfvrcld2  44045  uneqsn  44378  ntrneixb  44448  ntrneix3  44450  ntrneix13  44452  mnringmulrcld  44581  disjinfi  45548  salexct  46689  salexct2  46694  salexct3  46697  salgencntex  46698  salgensscntex  46699  nnfoctbdjlem  46810  nnfoctbdj  46811  iundjiun  46815  opprb  47388  euoreqb  47466  el1fzopredsuc  47682  iccpartgel  47786  paireqne  47868  divgcdoddALTV  48039  perfectALTVlem2  48079  clnbgrel  48185  dfvopnbgr2  48210  vopnbgrel  48211  dfclnbgr6  48213  dfnbgr6  48214  clnbgrgrim  48291  gpg5nbgrvtx03starlem1  48425  gpg5nbgrvtx03starlem2  48426  gpg5nbgrvtx03starlem3  48427  gpg5nbgrvtx13starlem1  48428  gpg5nbgrvtx13starlem2  48429  gpg5nbgrvtx13starlem3  48430  gpg5edgnedg  48487  lindslinindsimp2lem5  48819  ldepspr  48830  rrx2pnedifcoorneor  49073  rrx2plord  49077  rrx2plordisom  49080  itsclc0yqsol  49121