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  3666  sbcor  3788  unjust  3902  elun  4102  elprg  4600  eltpg  4640  el7g  4644  reuprg0  4656  rabsnifsb  4676  rabrsn  4678  preq12bg  4806  uniprg  4876  disji2  5079  disjprg  5091  disjxun  5093  swopolem  5539  sotrieq  5560  isso2i  5566  dmopab2rex  5863  somin1  6086  ordequn  6418  fununi  6563  unima  6905  unpreima  7004  eqfunresadj  7302  ordsucun  7763  funcnvuni  7870  fiunlem  7882  frxp  8064  xporderlem  8065  poxp  8066  fnwelem  8069  fnse  8071  xpord2lem  8080  poxp2  8081  xpord3lem  8087  poxp3  8088  soseq  8097  oacan  8471  omword  8493  oeword  8513  oeoa  8520  qsdisj  8726  wemapso2lem  9447  brwdom  9462  cantnflem1  9588  r0weon  9912  infxpen  9914  sornom  10177  fin1ai  10193  isfin5  10199  isfin6  10200  sdom2en01  10202  enfin2i  10221  enfin1ai  10284  isfin5-2  10291  fin1a2lem7  10306  fin1a2lem11  10310  fin1a2lem13  10312  axdc3lem2  10351  engch  10528  eltskg  10650  tsken  10654  ltsonq  10869  addcanpr  10946  ltsosr  10994  axpre-lttri  11065  lemul1  11982  mulge0b  12001  mulle0b  12002  mulsuble0b  12003  nn1m1nn  12155  avgle  12372  nn0sub  12440  elznn0  12492  elz2  12495  nneo  12565  uztric  12764  mul2lt0bi  13002  ltxr  13018  xrrebnd  13071  xmulval  13128  xmulneg1  13172  ixxun  13265  iccsplit  13389  fzsplit2  13453  uzsplit  13500  nelfzo  13568  fzospliti  13595  fzouzsplit  13598  sqeqor  14127  swrdnd  14566  sumeq1  15600  sumeq2w  15603  sumeq2ii  15604  sumeq2sdv  15614  fz1f1o  15621  summo  15628  fsum  15631  prodeq1f  15817  prodeq1  15818  prodeq2w  15821  prodeq2ii  15822  prodeq2sdv  15834  prodmo  15847  fprod  15852  ruclem12  16154  odd2np1lem  16255  dvdsprime  16602  coprm  16626  vdwapun  16890  vdwlem6  16902  vdwlem10  16906  mreexexlemd  17554  mreexexd  17558  istos  18326  tosso  18327  tleile  18329  resstos  18340  tsrlin  18495  tsrss  18499  islring  20459  isdomn  20624  prmirredlem  21413  domnchr  21473  zntoslem  21497  znfld  21501  fctop  22922  cctop  22924  ppttop  22925  pptbas  22926  isufil  23821  ufilss  23823  fixufil  23840  fin1aufil  23850  xpsdsval  24299  nlmmul0or  24601  pmltpclem1  25379  iundisj2  25480  mbfmax  25580  dvne0  25946  fta1glem2  26104  plymul0or  26218  ofmulrt  26219  quotval  26230  plydivlem3  26233  plydivlem4  26234  plydivex  26235  plydivalg  26237  quotlem  26238  aalioulem2  26271  quad2  26779  dcubic2  26784  dcubic  26786  dquartlem1  26791  dquart  26793  quart  26801  leibpilem2  26881  wilthlem1  27008  muval2  27074  perfectlem2  27171  lgslem1  27238  pntpbnd1  27527  slelss  27857  abssor  28187  n0s0suc  28273  n0s0m1  28291  nn1m1nns  28302  elzn0s  28325  elzs2  28326  zsoring  28335  n0seo  28347  zseo  28348  zs12zodd  28395  legtrid  28572  legso  28580  ishlg  28583  lnhl  28596  symquadlem  28670  islmib  28768  isinag  28819  isinagd  28820  inaghl  28826  brbtwn2  28887  axcontlem2  28947  axcontlem4  28949  axcontlem11  28956  edglnl  29125  nb3grprlem2  29363  hashecclwwlkn1  30061  nfrgr2v  30256  h1datom  31566  atss  32330  atom1d  32337  atord  32372  chirred  32379  elimifd  32527  disji2f  32561  disjif2  32565  disjxpin  32572  iundisj2f  32574  disjunsn  32578  brprop  32684  quad3d  32739  fzsplit3  32782  iundisj2fi  32786  f1ocnt  32789  trleile  32961  domnpropd  33252  subrdom  33260  isprmidl  33412  prmidlc  33422  qsidomlem1  33426  qsidomlem2  33427  mxidlmax  33439  rprmval  33490  isrprm  33491  smatrcl  33832  fsumcvg4  33986  erdsze2lem2  35271  satf  35420  satfv1  35430  satfbrsuc  35433  satfrnmapom  35437  satf0op  35444  sat1el2xp  35446  fmlafvel  35452  fmlasuc  35453  fmla1  35454  isfmlasuc  35455  fmlaomn0  35457  fmlasucdisj  35466  satffunlem1lem1  35469  satffunlem1lem2  35470  satffunlem2lem1  35471  dmopab3rexdif  35472  satffunlem2lem2  35473  satfv1fvfmla1  35490  2goelgoanfmla1  35491  satefvfmla1  35492  funpsstri  35833  seglelin  36183  lineunray  36214  prodeq12sdv  36285  cbvsumdavw  36346  cbvproddavw  36347  cbvsumdavw2  36362  cbvproddavw2  36363  weiunlem1  36529  topdifinffinlem  37414  topdifinffin  37415  topdifinfeq  37417  mblfinlem2  37721  itg2addnclem2  37735  iblabsnclem  37746  ftc1anclem5  37760  fdc1  37809  unichnidl  38094  ispridl  38097  maxidlmax  38106  disjressuc2  38458  qsdisjALTV  38734  lcvexchlem4  39159  lcvexchlem5  39160  2at0mat0  39647  pmapjoin  39974  cdlemg17h  40790  dihlspsnat  41455  lzunuz  42888  dvdsrabdioph  42930  acongeq12d  43099  jm2.25  43119  rmydioph  43134  expdioph  43143  fnwe2val  43169  aomclem8  43181  fzunt  43575  fzuntd  43576  fzunt1d  43577  fzuntgd  43578  sqrtcvallem1  43751  brfvrcld2  43812  uneqsn  44145  ntrneixb  44215  ntrneix3  44217  ntrneix13  44219  mnringmulrcld  44348  disjinfi  45316  salexct  46459  salexct2  46464  salexct3  46467  salgencntex  46468  salgensscntex  46469  nnfoctbdjlem  46580  nnfoctbdj  46581  iundjiun  46585  opprb  47158  euoreqb  47236  el1fzopredsuc  47452  iccpartgel  47556  paireqne  47638  divgcdoddALTV  47809  perfectALTVlem2  47849  clnbgrel  47955  dfvopnbgr2  47980  vopnbgrel  47981  dfclnbgr6  47983  dfnbgr6  47984  clnbgrgrim  48061  gpg5nbgrvtx03starlem1  48195  gpg5nbgrvtx03starlem2  48196  gpg5nbgrvtx03starlem3  48197  gpg5nbgrvtx13starlem1  48198  gpg5nbgrvtx13starlem2  48199  gpg5nbgrvtx13starlem3  48200  gpg5edgnedg  48257  lindslinindsimp2lem5  48590  ldepspr  48601  rrx2pnedifcoorneor  48844  rrx2plord  48848  rrx2plordisom  48851  itsclc0yqsol  48892