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  35717  satf  35866  satfv1  35876  satfbrsuc  35879  satfrnmapom  35883  satf0op  35890  sat1el2xp  35892  fmlafvel  35898  fmlasuc  35899  fmla1  35900  isfmlasuc  35901  fmlaomn0  35903  fmlasucdisj  35912  satffunlem1lem1  35915  satffunlem1lem2  35916  satffunlem2lem1  35917  dmopab3rexdif  35918  satffunlem2lem2  35919  satfv1fvfmla1  35936  2goelgoanfmla1  35937  satefvfmla1  35938  funpsstri  36279  seglelin  36629  lineunray  36660  ltnadd  36731  naddle  36732  prodeq12sdv  36771  cbvsumdavw  36832  cbvproddavw  36833  cbvsumdavw2  36848  cbvproddavw2  36849  weiunval  37014  axtcond  37030  topdifinffinlem  38034  topdifinffin  38035  topdifinfeq  38037  mblfinlem2  38350  itg2addnclem2  38364  iblabsnclem  38375  ftc1anclem5  38389  fdc1  38438  unichnidl  38723  ispridl  38726  maxidlmax  38735  disjressuc2  39101  qsdisjALTV  39389  lcvexchlem4  39852  lcvexchlem5  39853  2at0mat0  40340  pmapjoin  40667  cdlemg17h  41483  dihlspsnat  42148  quadfac  43013  lzunuz  43540  dvdsrabdioph  43578  acongeq12d  43747  jm2.25  43767  rmydioph  43782  expdioph  43791  fnwe2val  43817  aomclem8  43829  fzunt  44222  fzuntd  44223  fzunt1d  44224  fzuntgd  44225  sqrtcvallem1  44398  brfvrcld2  44459  uneqsn  44792  ntrneixb  44862  ntrneix3  44864  ntrneix13  44866  mnringmulrcld  44993  disjinfi  45951  salexct  47089  salexct2  47094  salexct3  47097  salgencntex  47098  salgensscntex  47099  nnfoctbdjlem  47210  nnfoctbdj  47211  iundjiun  47215  opprb  47809  euoreqb  47887  el1fzopredsuc  48104  iccpartgel  48219  paireqne  48301  divgcdoddALTV  48488  perfectALTVlem2  48528  clnbgrel  48634  dfvopnbgr2  48659  vopnbgrel  48660  dfclnbgr6  48662  dfnbgr6  48663  clnbgrgrim  48740  gpg5nbgrvtx03starlem1  48874  gpg5nbgrvtx03starlem2  48875  gpg5nbgrvtx03starlem3  48876  gpg5nbgrvtx13starlem1  48877  gpg5nbgrvtx13starlem2  48878  gpg5nbgrvtx13starlem3  48879  gpg5edgnedg  48936  lindslinindsimp2lem5  49283  ldepspr  49294  rrx2pnedifcoorneor  49537  rrx2plord  49541  rrx2plordisom  49544  itsclc0yqsol  49585