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  1610  eueq3  3673  sbcor  3795  unjust  3909  elun  4106  elprg  4602  eltpg  4640  el7g  4644  reuprg0  4656  rabsnifsb  4676  rabrsn  4678  preq12bg  4807  uniprg  4877  disji2  5079  disjprg  5091  disjxun  5093  swopolem  5541  sotrieq  5562  isso2i  5568  dmopab2rex  5864  somin1  6086  ordequn  6416  fununi  6561  unima  6902  unpreima  7001  eqfunresadj  7301  ordsucun  7764  funcnvuni  7872  fiunlem  7884  frxp  8066  xporderlem  8067  poxp  8068  fnwelem  8071  fnse  8073  xpord2lem  8082  poxp2  8083  xpord3lem  8089  poxp3  8090  soseq  8099  oacan  8473  omword  8495  oeword  8515  oeoa  8522  qsdisj  8728  wemapso2lem  9463  brwdom  9478  cantnflem1  9604  r0weon  9925  infxpen  9927  sornom  10190  fin1ai  10206  isfin5  10212  isfin6  10213  sdom2en01  10215  enfin2i  10234  enfin1ai  10297  isfin5-2  10304  fin1a2lem7  10319  fin1a2lem11  10323  fin1a2lem13  10325  axdc3lem2  10364  engch  10541  eltskg  10663  tsken  10667  ltsonq  10882  addcanpr  10959  ltsosr  11007  axpre-lttri  11078  lemul1  11994  mulge0b  12013  mulle0b  12014  mulsuble0b  12015  nn1m1nn  12167  avgle  12384  nn0sub  12452  elznn0  12504  elz2  12507  nneo  12578  uztric  12777  mul2lt0bi  13019  ltxr  13035  xrrebnd  13088  xmulval  13145  xmulneg1  13189  ixxun  13282  iccsplit  13406  fzsplit2  13470  uzsplit  13517  nelfzo  13585  fzospliti  13612  fzouzsplit  13615  sqeqor  14141  swrdnd  14579  sumeq1  15614  sumeq2w  15617  sumeq2ii  15618  sumeq2sdv  15628  fz1f1o  15635  summo  15642  fsum  15645  prodeq1f  15831  prodeq1  15832  prodeq2w  15835  prodeq2ii  15836  prodeq2sdv  15848  prodmo  15861  fprod  15866  ruclem12  16168  odd2np1lem  16269  dvdsprime  16616  coprm  16640  vdwapun  16904  vdwlem6  16916  vdwlem10  16920  mreexexlemd  17568  mreexexd  17572  istos  18340  tosso  18341  tleile  18343  resstos  18354  tsrlin  18509  tsrss  18513  islring  20443  isdomn  20608  prmirredlem  21397  domnchr  21457  zntoslem  21481  znfld  21485  fctop  22907  cctop  22909  ppttop  22910  pptbas  22911  isufil  23806  ufilss  23808  fixufil  23825  fin1aufil  23835  xpsdsval  24285  nlmmul0or  24587  pmltpclem1  25365  iundisj2  25466  mbfmax  25566  dvne0  25932  fta1glem2  26090  plymul0or  26204  ofmulrt  26205  quotval  26216  plydivlem3  26219  plydivlem4  26220  plydivex  26221  plydivalg  26223  quotlem  26224  aalioulem2  26257  quad2  26765  dcubic2  26770  dcubic  26772  dquartlem1  26777  dquart  26779  quart  26787  leibpilem2  26867  wilthlem1  26994  muval2  27060  perfectlem2  27157  lgslem1  27224  pntpbnd1  27513  slelss  27841  abssor  28171  n0s0suc  28257  n0s0m1  28275  nn1m1nns  28286  elzn0s  28309  elzs2  28310  zsoring  28319  n0seo  28331  zseo  28332  zs12zodd  28377  legtrid  28554  legso  28562  ishlg  28565  lnhl  28578  symquadlem  28652  islmib  28750  isinag  28801  isinagd  28802  inaghl  28808  brbtwn2  28868  axcontlem2  28928  axcontlem4  28930  axcontlem11  28937  edglnl  29106  nb3grprlem2  29344  hashecclwwlkn1  30039  nfrgr2v  30234  h1datom  31544  atss  32308  atom1d  32315  atord  32350  chirred  32357  elimifd  32505  disji2f  32539  disjif2  32543  disjxpin  32550  iundisj2f  32552  disjunsn  32556  brprop  32653  quad3d  32706  fzsplit3  32749  iundisj2fi  32753  f1ocnt  32758  trleile  32926  domnpropd  33229  subrdom  33237  isprmidl  33388  prmidlc  33398  qsidomlem1  33402  qsidomlem2  33403  mxidlmax  33415  rprmval  33466  isrprm  33467  smatrcl  33765  fsumcvg4  33919  erdsze2lem2  35179  satf  35328  satfv1  35338  satfbrsuc  35341  satfrnmapom  35345  satf0op  35352  sat1el2xp  35354  fmlafvel  35360  fmlasuc  35361  fmla1  35362  isfmlasuc  35363  fmlaomn0  35365  fmlasucdisj  35374  satffunlem1lem1  35377  satffunlem1lem2  35378  satffunlem2lem1  35379  dmopab3rexdif  35380  satffunlem2lem2  35381  satfv1fvfmla1  35398  2goelgoanfmla1  35399  satefvfmla1  35400  funpsstri  35741  seglelin  36092  lineunray  36123  prodeq12sdv  36194  cbvsumdavw  36255  cbvproddavw  36256  cbvsumdavw2  36271  cbvproddavw2  36272  weiunlem1  36438  topdifinffinlem  37323  topdifinffin  37324  topdifinfeq  37326  mblfinlem2  37640  itg2addnclem2  37654  iblabsnclem  37665  ftc1anclem5  37679  fdc1  37728  unichnidl  38013  ispridl  38016  maxidlmax  38025  disjressuc2  38362  qsdisjALTV  38594  lcvexchlem4  39018  lcvexchlem5  39019  2at0mat0  39507  pmapjoin  39834  cdlemg17h  40650  dihlspsnat  41315  lzunuz  42744  dvdsrabdioph  42786  acongeq12d  42955  jm2.25  42975  rmydioph  42990  expdioph  42999  fnwe2val  43025  aomclem8  43037  fzunt  43431  fzuntd  43432  fzunt1d  43433  fzuntgd  43434  sqrtcvallem1  43607  brfvrcld2  43668  uneqsn  44001  ntrneixb  44071  ntrneix3  44073  ntrneix13  44075  mnringmulrcld  44204  disjinfi  45173  salexct  46319  salexct2  46324  salexct3  46327  salgencntex  46328  salgensscntex  46329  nnfoctbdjlem  46440  nnfoctbdj  46441  iundjiun  46445  opprb  47019  euoreqb  47097  el1fzopredsuc  47313  iccpartgel  47417  paireqne  47499  divgcdoddALTV  47670  perfectALTVlem2  47710  clnbgrel  47816  dfvopnbgr2  47841  vopnbgrel  47842  dfclnbgr6  47844  dfnbgr6  47845  clnbgrgrim  47922  gpg5nbgrvtx03starlem1  48056  gpg5nbgrvtx03starlem2  48057  gpg5nbgrvtx03starlem3  48058  gpg5nbgrvtx13starlem1  48059  gpg5nbgrvtx13starlem2  48060  gpg5nbgrvtx13starlem3  48061  gpg5edgnedg  48118  lindslinindsimp2lem5  48451  ldepspr  48462  rrx2pnedifcoorneor  48705  rrx2plord  48709  rrx2plordisom  48712  itsclc0yqsol  48753