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  3657  sbcor  3779  unjust  3893  elun  4093  elprg  4590  eltpg  4630  el7g  4634  reuprg0  4646  rabsnifsb  4666  rabrsn  4668  preq12bg  4796  uniprg  4866  disji2  5069  disjprg  5081  disjxun  5083  axprg  5379  swopolem  5549  sotrieq  5570  isso2i  5576  dmopab2rex  5872  somin1  6096  ordequn  6428  fununi  6573  unima  6915  unpreima  7015  eqfunresadj  7315  ordsucun  7776  funcnvuni  7883  fiunlem  7895  frxp  8076  xporderlem  8077  poxp  8078  fnwelem  8081  fnse  8083  xpord2lem  8092  poxp2  8093  xpord3lem  8099  poxp3  8100  soseq  8109  oacan  8483  omword  8505  oeword  8526  oeoa  8533  qsdisj  8741  wemapso2lem  9467  brwdom  9482  cantnflem1  9610  r0weon  9934  infxpen  9936  sornom  10199  fin1ai  10215  isfin5  10221  isfin6  10222  sdom2en01  10224  enfin2i  10243  enfin1ai  10306  isfin5-2  10313  fin1a2lem7  10328  fin1a2lem11  10332  fin1a2lem13  10334  axdc3lem2  10373  engch  10551  eltskg  10673  tsken  10677  ltsonq  10892  addcanpr  10969  ltsosr  11017  axpre-lttri  11088  lemul1  12007  mulge0b  12026  mulle0b  12027  mulsuble0b  12028  nn1m1nn  12195  avgle  12419  nn0sub  12487  elznn0  12539  elz2  12542  nneo  12613  uztric  12812  mul2lt0bi  13050  ltxr  13066  xrrebnd  13120  xmulval  13177  xmulneg1  13221  ixxun  13314  iccsplit  13438  fzsplit2  13503  uzsplit  13550  nelfzo  13619  fzospliti  13646  fzouzsplit  13649  sqeqor  14178  swrdnd  14617  sumeq1  15651  sumeq2w  15654  sumeq2ii  15655  sumeq2sdv  15665  fz1f1o  15672  summo  15679  fsum  15682  prodeq1f  15871  prodeq1  15872  prodeq2w  15875  prodeq2ii  15876  prodeq2sdv  15888  prodmo  15901  fprod  15906  ruclem12  16208  odd2np1lem  16309  dvdsprime  16656  coprm  16681  vdwapun  16945  vdwlem6  16957  vdwlem10  16961  mreexexlemd  17610  mreexexd  17614  istos  18382  tosso  18383  tleile  18385  resstos  18396  tsrlin  18551  tsrss  18555  islring  20517  isdomn  20682  prmirredlem  21452  domnchr  21512  zntoslem  21536  znfld  21540  fctop  22969  cctop  22971  ppttop  22972  pptbas  22973  isufil  23868  ufilss  23870  fixufil  23887  fin1aufil  23897  xpsdsval  24346  nlmmul0or  24648  pmltpclem1  25415  iundisj2  25516  mbfmax  25616  dvne0  25978  fta1glem2  26134  plymul0or  26247  ofmulrt  26248  quotval  26258  plydivlem3  26261  plydivlem4  26262  plydivex  26263  plydivalg  26265  quotlem  26266  aalioulem2  26299  quad2  26803  dcubic2  26808  dcubic  26810  dquartlem1  26815  dquart  26817  quart  26825  leibpilem2  26905  wilthlem1  27031  muval2  27097  perfectlem2  27193  lgslem1  27260  pntpbnd1  27549  leslss  27901  abssor  28238  n0s0suc  28334  n0s0m1  28354  nn1m1nns  28366  elzn0s  28390  elzs2  28391  zsoring  28401  n0seo  28413  zseo  28414  bdayfinbndcbv  28458  bdayfinbndlem1  28459  bdayfinbndlem2  28460  bdayfinbnd  28461  z12zsodd  28474  legtrid  28659  legso  28667  ishlg  28670  lnhl  28683  symquadlem  28757  islmib  28855  isinag  28906  isinagd  28907  inaghl  28913  brbtwn2  28974  axcontlem2  29034  axcontlem4  29036  axcontlem11  29043  edglnl  29212  nb3grprlem2  29450  hashecclwwlkn1  30147  nfrgr2v  30342  h1datom  31653  atss  32417  atom1d  32424  atord  32459  chirred  32466  elimifd  32613  disji2f  32647  disjif2  32651  disjxpin  32658  iundisj2f  32660  disjunsn  32664  brprop  32770  quad3d  32822  fzsplit3  32866  iundisj2fi  32870  f1ocnt  32873  trleile  33031  domnpropd  33338  subrdom  33346  isprmidl  33498  prmidlc  33508  qsidomlem1  33512  qsidomlem2  33513  mxidlmax  33525  rprmval  33576  isrprm  33577  smatrcl  33940  fsumcvg4  34094  erdsze2lem2  35386  satf  35535  satfv1  35545  satfbrsuc  35548  satfrnmapom  35552  satf0op  35559  sat1el2xp  35561  fmlafvel  35567  fmlasuc  35568  fmla1  35569  isfmlasuc  35570  fmlaomn0  35572  fmlasucdisj  35581  satffunlem1lem1  35584  satffunlem1lem2  35585  satffunlem2lem1  35586  dmopab3rexdif  35587  satffunlem2lem2  35588  satfv1fvfmla1  35605  2goelgoanfmla1  35606  satefvfmla1  35607  funpsstri  35948  seglelin  36298  lineunray  36329  prodeq12sdv  36400  cbvsumdavw  36461  cbvproddavw  36462  cbvsumdavw2  36477  cbvproddavw2  36478  weiunval  36644  axtcond  36660  topdifinffinlem  37663  topdifinffin  37664  topdifinfeq  37666  mblfinlem2  37979  itg2addnclem2  37993  iblabsnclem  38004  ftc1anclem5  38018  fdc1  38067  unichnidl  38352  ispridl  38355  maxidlmax  38364  disjressuc2  38732  qsdisjALTV  39020  lcvexchlem4  39483  lcvexchlem5  39484  2at0mat0  39971  pmapjoin  40298  cdlemg17h  41114  dihlspsnat  41779  lzunuz  43200  dvdsrabdioph  43238  acongeq12d  43407  jm2.25  43427  rmydioph  43442  expdioph  43451  fnwe2val  43477  aomclem8  43489  fzunt  43882  fzuntd  43883  fzunt1d  43884  fzuntgd  43885  sqrtcvallem1  44058  brfvrcld2  44119  uneqsn  44452  ntrneixb  44522  ntrneix3  44524  ntrneix13  44526  mnringmulrcld  44655  disjinfi  45622  salexct  46762  salexct2  46767  salexct3  46770  salgencntex  46771  salgensscntex  46772  nnfoctbdjlem  46883  nnfoctbdj  46884  iundjiun  46888  opprb  47479  euoreqb  47557  el1fzopredsuc  47774  iccpartgel  47889  paireqne  47971  divgcdoddALTV  48158  perfectALTVlem2  48198  clnbgrel  48304  dfvopnbgr2  48329  vopnbgrel  48330  dfclnbgr6  48332  dfnbgr6  48333  clnbgrgrim  48410  gpg5nbgrvtx03starlem1  48544  gpg5nbgrvtx03starlem2  48545  gpg5nbgrvtx03starlem3  48546  gpg5nbgrvtx13starlem1  48547  gpg5nbgrvtx13starlem2  48548  gpg5nbgrvtx13starlem3  48549  gpg5edgnedg  48606  lindslinindsimp2lem5  48938  ldepspr  48949  rrx2pnedifcoorneor  49192  rrx2plord  49196  rrx2plordisom  49199  itsclc0yqsol  49240