Theorem orbi12d 924

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

Syntax hints:   → wi 4   ↔ wb 207   ∨ wo 853

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 208  df-or 854

This theorem is referenced by:  pm4.39  984  ifpbi123d  1084  3orbi123d  1443  cadbi123d  1617  eueq3  3659  sbcor  3780  unjust  3894  elun  4090  elprg  4585  eltpg  4625  el7g  4629  reuprg0  4641  rabsnifsb  4661  rabrsn  4663  preq12bg  4791  uniprg  4861  disji2  5063  disjprg  5075  disjxun  5077  axprg  5373  swopolem  5543  sotrieq  5564  isso2i  5570  dmopab2rex  5866  somin1  6090  ordequn  6422  fununi  6567  unima  6909  unpreima  7011  eqfunresadj  7311  ordsucun  7772  funcnvuni  7879  fiunlem  7891  frxp  8073  xporderlem  8074  poxp  8075  fnwelem  8078  fnse  8080  xpord2lem  8089  poxp2  8090  xpord3lem  8096  poxp3  8097  soseq  8106  oacan  8480  omword  8502  oeword  8523  oeoa  8530  qsdisj  8738  wemapso2lem  9464  brwdom  9479  cantnflem1  9608  r0weon  9932  infxpen  9934  sornom  10197  fin1ai  10213  isfin5  10219  isfin6  10220  sdom2en01  10222  enfin2i  10241  enfin1ai  10304  isfin5-2  10311  fin1a2lem7  10326  fin1a2lem11  10330  fin1a2lem13  10332  axdc3lem2  10371  engch  10549  eltskg  10671  tsken  10675  ltsonq  10890  addcanpr  10967  ltsosr  11015  axpre-lttri  11086  lemul1  12005  mulge0b  12024  mulle0b  12025  mulsuble0b  12026  nn1m1nn  12193  avgle  12417  nn0sub  12485  elznn0  12537  elz2  12540  nneo  12611  uztric  12810  mul2lt0bi  13048  ltxr  13064  xrrebnd  13118  xmulval  13175  xmulneg1  13219  ixxun  13312  iccsplit  13436  fzsplit2  13501  uzsplit  13548  nelfzo  13617  fzospliti  13644  fzouzsplit  13647  sqeqor  14176  swrdnd  14615  sumeq1  15649  sumeq2w  15652  sumeq2ii  15653  sumeq2sdv  15663  fz1f1o  15670  summo  15677  fsum  15680  prodeq1f  15869  prodeq1  15870  prodeq2w  15873  prodeq2ii  15874  prodeq2sdv  15886  prodmo  15899  fprod  15904  ruclem12  16206  odd2np1lem  16307  dvdsprime  16654  coprm  16679  vdwapun  16943  vdwlem6  16955  vdwlem10  16959  mreexexlemd  17608  mreexexd  17612  istos  18380  tosso  18381  tleile  18383  resstos  18394  tsrlin  18549  tsrss  18553  islring  20519  isdomn  20684  prmirredlem  21454  domnchr  21514  zntoslem  21538  znfld  21542  fctop  22994  cctop  22996  ppttop  22997  pptbas  22998  isufil  23893  ufilss  23895  fixufil  23912  fin1aufil  23922  xpsdsval  24371  nlmmul0or  24673  pmltpclem1  25440  iundisj2  25541  mbfmax  25641  dvne0  26003  fta1glem2  26159  plymul0or  26272  ofmulrt  26273  quotval  26283  plydivlem3  26286  plydivlem4  26287  plydivex  26288  plydivalg  26290  quotlem  26291  aalioulem2  26324  quad2  26828  dcubic2  26833  dcubic  26835  dquartlem1  26840  dquart  26842  quart  26850  leibpilem2  26930  wilthlem1  27056  muval2  27122  perfectlem2  27218  lgslem1  27285  pntpbnd1  27574  leslss  27926  abssor  28263  n0s0suc  28359  n0s0m1  28379  nn1m1nns  28391  elzn0s  28415  elzs2  28416  zsoring  28426  n0seo  28438  zseo  28439  bdayfinbndcbv  28483  bdayfinbndlem1  28484  bdayfinbndlem2  28485  bdayfinbnd  28486  z12zsodd  28499  legtrid  28684  legso  28692  ishlg  28695  lnhl  28708  symquadlem  28782  islmib  28880  isinag  28931  isinagd  28932  inaghl  28938  brbtwn2  28999  axcontlem2  29059  axcontlem4  29061  axcontlem11  29068  edglnl  29237  nb3grprlem2  29475  hashecclwwlkn1  30172  nfrgr2v  30367  h1datom  31678  atss  32442  atom1d  32449  atord  32484  chirred  32491  elimifd  32638  disji2f  32673  disjif2  32677  disjxpin  32684  iundisj2f  32686  disjunsn  32690  brprop  32796  quad3d  32848  fzsplit3  32892  iundisj2fi  32896  f1ocnt  32899  trleile  33057  domnpropd  33365  subrdom  33373  isprmidl  33528  prmidlc  33538  qsidomlem1  33542  qsidomlem2  33543  mxidlmax  33555  rprmval  33606  isrprm  33607  smatrcl  33987  fsumcvg4  34141  erdsze2lem2  35439  satf  35588  satfv1  35598  satfbrsuc  35601  satfrnmapom  35605  satf0op  35612  sat1el2xp  35614  fmlafvel  35620  fmlasuc  35621  fmla1  35622  isfmlasuc  35623  fmlaomn0  35625  fmlasucdisj  35634  satffunlem1lem1  35637  satffunlem1lem2  35638  satffunlem2lem1  35639  dmopab3rexdif  35640  satffunlem2lem2  35641  satfv1fvfmla1  35658  2goelgoanfmla1  35659  satefvfmla1  35660  funpsstri  36001  seglelin  36351  lineunray  36382  prodeq12sdv  36453  cbvsumdavw  36514  cbvproddavw  36515  cbvsumdavw2  36530  cbvproddavw2  36531  weiunval  36697  axtcond  36713  topdifinffinlem  37716  topdifinffin  37717  topdifinfeq  37719  mblfinlem2  38032  itg2addnclem2  38046  iblabsnclem  38057  ftc1anclem5  38071  fdc1  38120  unichnidl  38405  ispridl  38408  maxidlmax  38417  disjressuc2  38785  qsdisjALTV  39073  lcvexchlem4  39536  lcvexchlem5  39537  2at0mat0  40024  pmapjoin  40351  cdlemg17h  41167  dihlspsnat  41832  lzunuz  43224  dvdsrabdioph  43262  acongeq12d  43431  jm2.25  43451  rmydioph  43466  expdioph  43475  fnwe2val  43501  aomclem8  43513  fzunt  43906  fzuntd  43907  fzunt1d  43908  fzuntgd  43909  sqrtcvallem1  44082  brfvrcld2  44143  uneqsn  44476  ntrneixb  44546  ntrneix3  44548  ntrneix13  44550  mnringmulrcld  44679  disjinfi  45646  salexct  46784  salexct2  46789  salexct3  46792  salgencntex  46793  salgensscntex  46794  nnfoctbdjlem  46905  nnfoctbdj  46906  iundjiun  46910  opprb  47501  euoreqb  47579  el1fzopredsuc  47796  iccpartgel  47911  paireqne  47993  divgcdoddALTV  48180  perfectALTVlem2  48220  clnbgrel  48326  dfvopnbgr2  48351  vopnbgrel  48352  dfclnbgr6  48354  dfnbgr6  48355  clnbgrgrim  48432  gpg5nbgrvtx03starlem1  48566  gpg5nbgrvtx03starlem2  48567  gpg5nbgrvtx03starlem3  48568  gpg5nbgrvtx13starlem1  48569  gpg5nbgrvtx13starlem2  48570  gpg5nbgrvtx13starlem3  48571  gpg5edgnedg  48628  lindslinindsimp2lem5  48960  ldepspr  48971  rrx2pnedifcoorneor  49214  rrx2plord  49218  rrx2plordisom  49221  itsclc0yqsol  49262