Theorem orbi12d 932

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  pm4.39  992  ifpbi123d  1095  3orbi123d  1463  cadbi123d  1643  eueq3  3677  sbcor  3797  unjust  3912  elun  4110  elprg  4617  eltpg  4657  el7g  4661  reuprg0  4673  rabsnifsb  4693  rabrsn  4695  preq12bg  4823  uniprg  4893  disji2  5098  disjprg  5110  disjxun  5112  axprg  5413  swopolem  5584  sotrieq  5605  isso2i  5611  dmopab2rex  5912  somin1  6138  ordequn  6473  fununi  6618  unima  6963  unpreima  7065  eqfunresadj  7371  ordsucun  7830  funcnvuni  7938  fiunlem  7948  frxp  8131  xporderlem  8132  poxp  8133  fnwelem  8136  fnse  8138  xpord2lem  8147  poxp2  8148  xpord3lem  8154  poxp3  8155  soseq  8164  oacan  8542  omword  8564  oeword  8585  oeoa  8592  qsdisj  8801  wemapso2lem  9524  brwdom  9539  cantnflem1  9668  r0weon  10015  infxpen  10017  sornom  10279  fin1ai  10295  isfin5  10301  isfin6  10302  sdom2en01  10304  enfin2i  10323  enfin1ai  10386  isfin5-2  10393  fin1a2lem7  10408  fin1a2lem11  10412  fin1a2lem13  10414  axdc3lem2  10453  engch  10631  eltskg  10753  tsken  10757  ltsonq  10972  addcanpr  11049  ltsosr  11097  axpre-lttri  11168  lemul1  12085  mulge0b  12103  mulle0b  12104  mulsuble0b  12105  nn1m1nn  12272  avgle  12504  nn0sub  12572  elznn0  12624  elz2  12627  nneo  12698  uztric  12904  mul2lt0bi  13142  ltxr  13158  xrrebnd  13212  xmulval  13269  xmulneg1  13313  ixxun  13406  iccsplit  13530  fzsplit2  13596  uzsplit  13643  nelfzo  13712  fzospliti  13739  fzouzsplit  13742  sqeqor  14272  swrdnd  14716  sumeq1  15766  sumeq2w  15769  sumeq2ii  15770  sumeq2sdv  15780  fz1f1o  15787  summo  15794  fsum  15797  prodeq1f  15986  prodeq1  15987  prodeq2w  15990  prodeq2ii  15991  prodeq2sdv  16003  prodmo  16016  fprod  16021  ruclem12  16322  odd2np1lem  16423  dvdsprime  16770  coprm  16795  vdwapun  17059  vdwlem6  17071  vdwlem10  17075  mreexexlemd  17725  mreexexd  17729  istos  18497  tosso  18498  tleile  18500  resstos  18511  tsrlin  18666  tsrss  18670  islring  20676  isdomn  20841  unichnlidl  21399  isprmidl  21500  prmidlc  21510  qsidomlem1  21517  qsidomlem2  21518  prmirredlem  21659  domnchr  21719  zntoslem  21743  znfld  21747  fctop  23198  cctop  23200  ppttop  23201  pptbas  23202  isufil  24097  ufilss  24099  fixufil  24116  fin1aufil  24126  xpsdsval  24575  nlmmul0or  24877  pmltpclem1  25644  iundisj2  25745  mbfmax  25845  dvne0  26207  fta1glem2  26363  plymul0or  26476  ofmulrt  26477  quotval  26490  plydivlem3  26493  plydivlem4  26494  plydivex  26495  plydivalg  26497  quotlem  26498  aalioulem2  26533  quad2  27041  dcubic2  27046  dcubic  27048  dquartlem1  27053  dquart  27055  quart  27063  leibpilem2  27143  wilthlem1  27269  muval2  27335  perfectlem2  27431  lgslem1  27498  pntpbnd1  27787  leslss  28139  abssor  28476  n0s0suc  28572  n0s0m1  28592  nn1m1nns  28604  elzn0s  28628  elzs2  28629  zsoring  28639  n0seo  28651  zseo  28652  bdayfinbndcbv  28696  bdayfinbndlem1  28697  bdayfinbndlem2  28698  bdayfinbnd  28699  z12zsodd  28712  legtrid  28897  legso  28905  ishlg2  28908  ishlg  28911  lnhl  28924  symquadlem  29003  plngcplem  29104  islmib  29133  isinag  29192  isinagd  29193  inaghl  29199  brprlng  29225  brbtwn2  29292  axcontlem2  29352  axcontlem4  29354  axcontlem11  29361  edglnl  29530  nb3grprlem2  29768  hashecclwwlkn1  30465  nfrgr2v  30660  h1datom  31971  atss  32735  atom1d  32742  atord  32777  chirred  32784  elimifd  32926  disji2f  32959  disjif2  32963  disjxpin  32970  iundisj2f  32972  disjunsn  32976  brprop  33079  quad3d  33131  fzsplit3  33175  iundisj2fi  33179  f1ocnt  33182  trleile  33322  domnpropd  33631  subrdom  33636  mxidlmax  33779  rprmval  33837  isrprm  33838  smatrcl  34217  fsumcvg4  34371  erdsze2lem2  35716  satf  35865  satfv1  35875  satfbrsuc  35878  satfrnmapom  35882  satf0op  35889  sat1el2xp  35891  fmlafvel  35897  fmlasuc  35898  fmla1  35899  isfmlasuc  35900  fmlaomn0  35902  fmlasucdisj  35911  satffunlem1lem1  35914  satffunlem1lem2  35915  satffunlem2lem1  35916  dmopab3rexdif  35917  satffunlem2lem2  35918  satfv1fvfmla1  35935  2goelgoanfmla1  35936  satefvfmla1  35937  funpsstri  36278  seglelin  36628  lineunray  36659  ltnadd  36730  naddle  36731  prodeq12sdv  36770  cbvsumdavw  36831  cbvproddavw  36832  cbvsumdavw2  36847  cbvproddavw2  36848  weiunval  37013  axtcond  37029  topdifinffinlem  38033  topdifinffin  38034  topdifinfeq  38036  mblfinlem2  38349  itg2addnclem2  38363  iblabsnclem  38374  ftc1anclem5  38388  fdc1  38437  unichnidl  38722  ispridl  38725  maxidlmax  38734  disjressuc2  39100  qsdisjALTV  39388  lcvexchlem4  39851  lcvexchlem5  39852  2at0mat0  40339  pmapjoin  40666  cdlemg17h  41482  dihlspsnat  42147  quadfac  43012  lzunuz  43539  dvdsrabdioph  43577  acongeq12d  43746  jm2.25  43766  rmydioph  43781  expdioph  43790  fnwe2val  43816  aomclem8  43828  fzunt  44221  fzuntd  44222  fzunt1d  44223  fzuntgd  44224  sqrtcvallem1  44397  brfvrcld2  44458  uneqsn  44791  ntrneixb  44861  ntrneix3  44863  ntrneix13  44865  mnringmulrcld  44992  disjinfi  45950  salexct  47088  salexct2  47093  salexct3  47096  salgencntex  47097  salgensscntex  47098  nnfoctbdjlem  47209  nnfoctbdj  47210  iundjiun  47214  opprb  47808  euoreqb  47886  el1fzopredsuc  48103  iccpartgel  48218  paireqne  48300  divgcdoddALTV  48487  perfectALTVlem2  48527  clnbgrel  48633  dfvopnbgr2  48658  vopnbgrel  48659  dfclnbgr6  48661  dfnbgr6  48662  clnbgrgrim  48739  gpg5nbgrvtx03starlem1  48873  gpg5nbgrvtx03starlem2  48874  gpg5nbgrvtx03starlem3  48875  gpg5nbgrvtx13starlem1  48876  gpg5nbgrvtx13starlem2  48877  gpg5nbgrvtx13starlem3  48878  gpg5edgnedg  48935  lindslinindsimp2lem5  49282  ldepspr  49293  rrx2pnedifcoorneor  49536  rrx2plord  49540  rrx2plordisom  49543  itsclc0yqsol  49584