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  3658  sbcor  3780  unjust  3894  elun  4094  elprg  4591  eltpg  4631  el7g  4635  reuprg0  4647  rabsnifsb  4667  rabrsn  4669  preq12bg  4797  uniprg  4867  disji2  5070  disjprg  5082  disjxun  5084  axprg  5374  swopolem  5542  sotrieq  5563  isso2i  5569  dmopab2rex  5866  somin1  6090  ordequn  6422  fununi  6567  unima  6909  unpreima  7009  eqfunresadj  7308  ordsucun  7769  funcnvuni  7876  fiunlem  7888  frxp  8069  xporderlem  8070  poxp  8071  fnwelem  8074  fnse  8076  xpord2lem  8085  poxp2  8086  xpord3lem  8092  poxp3  8093  soseq  8102  oacan  8476  omword  8498  oeword  8519  oeoa  8526  qsdisj  8734  wemapso2lem  9460  brwdom  9475  cantnflem1  9601  r0weon  9925  infxpen  9927  sornom  10190  fin1ai  10206  isfin5  10212  isfin6  10213  sdom2en01  10215  enfin2i  10234  enfin1ai  10297  isfin5-2  10304  fin1a2lem7  10319  fin1a2lem11  10323  fin1a2lem13  10325  axdc3lem2  10364  engch  10542  eltskg  10664  tsken  10668  ltsonq  10883  addcanpr  10960  ltsosr  11008  axpre-lttri  11079  lemul1  11998  mulge0b  12017  mulle0b  12018  mulsuble0b  12019  nn1m1nn  12186  avgle  12410  nn0sub  12478  elznn0  12530  elz2  12533  nneo  12604  uztric  12803  mul2lt0bi  13041  ltxr  13057  xrrebnd  13111  xmulval  13168  xmulneg1  13212  ixxun  13305  iccsplit  13429  fzsplit2  13494  uzsplit  13541  nelfzo  13610  fzospliti  13637  fzouzsplit  13640  sqeqor  14169  swrdnd  14608  sumeq1  15642  sumeq2w  15645  sumeq2ii  15646  sumeq2sdv  15656  fz1f1o  15663  summo  15670  fsum  15673  prodeq1f  15862  prodeq1  15863  prodeq2w  15866  prodeq2ii  15867  prodeq2sdv  15879  prodmo  15892  fprod  15897  ruclem12  16199  odd2np1lem  16300  dvdsprime  16647  coprm  16672  vdwapun  16936  vdwlem6  16948  vdwlem10  16952  mreexexlemd  17601  mreexexd  17605  istos  18373  tosso  18374  tleile  18376  resstos  18387  tsrlin  18542  tsrss  18546  islring  20508  isdomn  20673  prmirredlem  21462  domnchr  21522  zntoslem  21546  znfld  21550  fctop  22979  cctop  22981  ppttop  22982  pptbas  22983  isufil  23878  ufilss  23880  fixufil  23897  fin1aufil  23907  xpsdsval  24356  nlmmul0or  24658  pmltpclem1  25425  iundisj2  25526  mbfmax  25626  dvne0  25988  fta1glem2  26144  plymul0or  26257  ofmulrt  26258  quotval  26269  plydivlem3  26272  plydivlem4  26273  plydivex  26274  plydivalg  26276  quotlem  26277  aalioulem2  26310  quad2  26816  dcubic2  26821  dcubic  26823  dquartlem1  26828  dquart  26830  quart  26838  leibpilem2  26918  wilthlem1  27045  muval2  27111  perfectlem2  27207  lgslem1  27274  pntpbnd1  27563  leslss  27915  abssor  28252  n0s0suc  28348  n0s0m1  28368  nn1m1nns  28380  elzn0s  28404  elzs2  28405  zsoring  28415  n0seo  28427  zseo  28428  bdayfinbndcbv  28472  bdayfinbndlem1  28473  bdayfinbndlem2  28474  bdayfinbnd  28475  z12zsodd  28488  legtrid  28673  legso  28681  ishlg  28684  lnhl  28697  symquadlem  28771  islmib  28869  isinag  28920  isinagd  28921  inaghl  28927  brbtwn2  28988  axcontlem2  29048  axcontlem4  29050  axcontlem11  29057  edglnl  29226  nb3grprlem2  29464  hashecclwwlkn1  30162  nfrgr2v  30357  h1datom  31668  atss  32432  atom1d  32439  atord  32474  chirred  32481  elimifd  32628  disji2f  32662  disjif2  32666  disjxpin  32673  iundisj2f  32675  disjunsn  32679  brprop  32785  quad3d  32837  fzsplit3  32881  iundisj2fi  32885  f1ocnt  32888  trleile  33046  domnpropd  33353  subrdom  33361  isprmidl  33513  prmidlc  33523  qsidomlem1  33527  qsidomlem2  33528  mxidlmax  33540  rprmval  33591  isrprm  33592  smatrcl  33956  fsumcvg4  34110  erdsze2lem2  35402  satf  35551  satfv1  35561  satfbrsuc  35564  satfrnmapom  35568  satf0op  35575  sat1el2xp  35577  fmlafvel  35583  fmlasuc  35584  fmla1  35585  isfmlasuc  35586  fmlaomn0  35588  fmlasucdisj  35597  satffunlem1lem1  35600  satffunlem1lem2  35601  satffunlem2lem1  35602  dmopab3rexdif  35603  satffunlem2lem2  35604  satfv1fvfmla1  35621  2goelgoanfmla1  35622  satefvfmla1  35623  funpsstri  35964  seglelin  36314  lineunray  36345  prodeq12sdv  36416  cbvsumdavw  36477  cbvproddavw  36478  cbvsumdavw2  36493  cbvproddavw2  36494  weiunval  36660  axtcond  36676  topdifinffinlem  37677  topdifinffin  37678  topdifinfeq  37680  mblfinlem2  37993  itg2addnclem2  38007  iblabsnclem  38018  ftc1anclem5  38032  fdc1  38081  unichnidl  38366  ispridl  38369  maxidlmax  38378  disjressuc2  38746  qsdisjALTV  39034  lcvexchlem4  39497  lcvexchlem5  39498  2at0mat0  39985  pmapjoin  40312  cdlemg17h  41128  dihlspsnat  41793  lzunuz  43214  dvdsrabdioph  43256  acongeq12d  43425  jm2.25  43445  rmydioph  43460  expdioph  43469  fnwe2val  43495  aomclem8  43507  fzunt  43900  fzuntd  43901  fzunt1d  43902  fzuntgd  43903  sqrtcvallem1  44076  brfvrcld2  44137  uneqsn  44470  ntrneixb  44540  ntrneix3  44542  ntrneix13  44544  mnringmulrcld  44673  disjinfi  45640  salexct  46780  salexct2  46785  salexct3  46788  salgencntex  46789  salgensscntex  46790  nnfoctbdjlem  46901  nnfoctbdj  46902  iundjiun  46906  opprb  47491  euoreqb  47569  el1fzopredsuc  47786  iccpartgel  47901  paireqne  47983  divgcdoddALTV  48170  perfectALTVlem2  48210  clnbgrel  48316  dfvopnbgr2  48341  vopnbgrel  48342  dfclnbgr6  48344  dfnbgr6  48345  clnbgrgrim  48422  gpg5nbgrvtx03starlem1  48556  gpg5nbgrvtx03starlem2  48557  gpg5nbgrvtx03starlem3  48558  gpg5nbgrvtx13starlem1  48559  gpg5nbgrvtx13starlem2  48560  gpg5nbgrvtx13starlem3  48561  gpg5edgnedg  48618  lindslinindsimp2lem5  48950  ldepspr  48961  rrx2pnedifcoorneor  49204  rrx2plord  49208  rrx2plordisom  49211  itsclc0yqsol  49252