Theorem orbi12d 918

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

Syntax hints:   → wi 4   ↔ wb 206   ∨ wo 847

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 848

This theorem is referenced by:  pm4.39  978  ifpbi123d  1078  3orbi123d  1437  cadbi123d  1611  eueq3  3669  sbcor  3791  unjust  3905  elun  4105  elprg  4603  eltpg  4643  el7g  4647  reuprg0  4659  rabsnifsb  4679  rabrsn  4681  preq12bg  4809  uniprg  4879  disji2  5082  disjprg  5094  disjxun  5096  swopolem  5542  sotrieq  5563  isso2i  5569  dmopab2rex  5866  somin1  6090  ordequn  6422  fununi  6567  unima  6909  unpreima  7008  eqfunresadj  7306  ordsucun  7767  funcnvuni  7874  fiunlem  7886  frxp  8068  xporderlem  8069  poxp  8070  fnwelem  8073  fnse  8075  xpord2lem  8084  poxp2  8085  xpord3lem  8091  poxp3  8092  soseq  8101  oacan  8475  omword  8497  oeword  8518  oeoa  8525  qsdisj  8731  wemapso2lem  9457  brwdom  9472  cantnflem1  9598  r0weon  9922  infxpen  9924  sornom  10187  fin1ai  10203  isfin5  10209  isfin6  10210  sdom2en01  10212  enfin2i  10231  enfin1ai  10294  isfin5-2  10301  fin1a2lem7  10316  fin1a2lem11  10320  fin1a2lem13  10322  axdc3lem2  10361  engch  10539  eltskg  10661  tsken  10665  ltsonq  10880  addcanpr  10957  ltsosr  11005  axpre-lttri  11076  lemul1  11993  mulge0b  12012  mulle0b  12013  mulsuble0b  12014  nn1m1nn  12166  avgle  12383  nn0sub  12451  elznn0  12503  elz2  12506  nneo  12576  uztric  12775  mul2lt0bi  13013  ltxr  13029  xrrebnd  13083  xmulval  13140  xmulneg1  13184  ixxun  13277  iccsplit  13401  fzsplit2  13465  uzsplit  13512  nelfzo  13580  fzospliti  13607  fzouzsplit  13610  sqeqor  14139  swrdnd  14578  sumeq1  15612  sumeq2w  15615  sumeq2ii  15616  sumeq2sdv  15626  fz1f1o  15633  summo  15640  fsum  15643  prodeq1f  15829  prodeq1  15830  prodeq2w  15833  prodeq2ii  15834  prodeq2sdv  15846  prodmo  15859  fprod  15864  ruclem12  16166  odd2np1lem  16267  dvdsprime  16614  coprm  16638  vdwapun  16902  vdwlem6  16914  vdwlem10  16918  mreexexlemd  17567  mreexexd  17571  istos  18339  tosso  18340  tleile  18342  resstos  18353  tsrlin  18508  tsrss  18512  islring  20473  isdomn  20638  prmirredlem  21427  domnchr  21487  zntoslem  21511  znfld  21515  fctop  22948  cctop  22950  ppttop  22951  pptbas  22952  isufil  23847  ufilss  23849  fixufil  23866  fin1aufil  23876  xpsdsval  24325  nlmmul0or  24627  pmltpclem1  25405  iundisj2  25506  mbfmax  25606  dvne0  25972  fta1glem2  26130  plymul0or  26244  ofmulrt  26245  quotval  26256  plydivlem3  26259  plydivlem4  26260  plydivex  26261  plydivalg  26263  quotlem  26264  aalioulem2  26297  quad2  26805  dcubic2  26810  dcubic  26812  dquartlem1  26817  dquart  26819  quart  26827  leibpilem2  26907  wilthlem1  27034  muval2  27100  perfectlem2  27197  lgslem1  27264  pntpbnd1  27553  leslss  27905  abssor  28242  n0s0suc  28338  n0s0m1  28358  nn1m1nns  28370  elzn0s  28394  elzs2  28395  zsoring  28405  n0seo  28417  zseo  28418  bdayfinbndcbv  28462  bdayfinbndlem1  28463  bdayfinbndlem2  28464  bdayfinbnd  28465  z12zsodd  28478  legtrid  28663  legso  28671  ishlg  28674  lnhl  28687  symquadlem  28761  islmib  28859  isinag  28910  isinagd  28911  inaghl  28917  brbtwn2  28978  axcontlem2  29038  axcontlem4  29040  axcontlem11  29047  edglnl  29216  nb3grprlem2  29454  hashecclwwlkn1  30152  nfrgr2v  30347  h1datom  31657  atss  32421  atom1d  32428  atord  32463  chirred  32470  elimifd  32618  disji2f  32652  disjif2  32656  disjxpin  32663  iundisj2f  32665  disjunsn  32669  brprop  32776  quad3d  32829  fzsplit3  32873  iundisj2fi  32877  f1ocnt  32880  trleile  33053  domnpropd  33359  subrdom  33367  isprmidl  33519  prmidlc  33529  qsidomlem1  33533  qsidomlem2  33534  mxidlmax  33546  rprmval  33597  isrprm  33598  smatrcl  33953  fsumcvg4  34107  erdsze2lem2  35398  satf  35547  satfv1  35557  satfbrsuc  35560  satfrnmapom  35564  satf0op  35571  sat1el2xp  35573  fmlafvel  35579  fmlasuc  35580  fmla1  35581  isfmlasuc  35582  fmlaomn0  35584  fmlasucdisj  35593  satffunlem1lem1  35596  satffunlem1lem2  35597  satffunlem2lem1  35598  dmopab3rexdif  35599  satffunlem2lem2  35600  satfv1fvfmla1  35617  2goelgoanfmla1  35618  satefvfmla1  35619  funpsstri  35960  seglelin  36310  lineunray  36341  prodeq12sdv  36412  cbvsumdavw  36473  cbvproddavw  36474  cbvsumdavw2  36489  cbvproddavw2  36490  weiunval  36656  topdifinffinlem  37552  topdifinffin  37553  topdifinfeq  37555  mblfinlem2  37859  itg2addnclem2  37873  iblabsnclem  37884  ftc1anclem5  37898  fdc1  37947  unichnidl  38232  ispridl  38235  maxidlmax  38244  disjressuc2  38596  qsdisjALTV  38872  lcvexchlem4  39297  lcvexchlem5  39298  2at0mat0  39785  pmapjoin  40112  cdlemg17h  40928  dihlspsnat  41593  lzunuz  43010  dvdsrabdioph  43052  acongeq12d  43221  jm2.25  43241  rmydioph  43256  expdioph  43265  fnwe2val  43291  aomclem8  43303  fzunt  43696  fzuntd  43697  fzunt1d  43698  fzuntgd  43699  sqrtcvallem1  43872  brfvrcld2  43933  uneqsn  44266  ntrneixb  44336  ntrneix3  44338  ntrneix13  44340  mnringmulrcld  44469  disjinfi  45436  salexct  46578  salexct2  46583  salexct3  46586  salgencntex  46587  salgensscntex  46588  nnfoctbdjlem  46699  nnfoctbdj  46700  iundjiun  46704  opprb  47277  euoreqb  47355  el1fzopredsuc  47571  iccpartgel  47675  paireqne  47757  divgcdoddALTV  47928  perfectALTVlem2  47968  clnbgrel  48074  dfvopnbgr2  48099  vopnbgrel  48100  dfclnbgr6  48102  dfnbgr6  48103  clnbgrgrim  48180  gpg5nbgrvtx03starlem1  48314  gpg5nbgrvtx03starlem2  48315  gpg5nbgrvtx03starlem3  48316  gpg5nbgrvtx13starlem1  48317  gpg5nbgrvtx13starlem2  48318  gpg5nbgrvtx13starlem3  48319  gpg5edgnedg  48376  lindslinindsimp2lem5  48708  ldepspr  48719  rrx2pnedifcoorneor  48962  rrx2plord  48966  rrx2plordisom  48969  itsclc0yqsol  49010