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  1434  cadbi123d  1606  eueq3  3719  sbcor  3844  unjust  3966  elun  4162  elprg  4652  eltpg  4690  el7g  4694  reuprg0  4706  rabsnifsb  4726  rabrsn  4728  preq12bg  4857  uniprg  4927  disji2  5131  disjprg  5143  disjxun  5145  swopolem  5606  sotrieq  5626  isso2i  5632  dmopab2rex  5930  somin1  6155  ordequn  6488  fununi  6642  unima  6983  unpreima  7082  eqfunresadj  7379  ordsucun  7844  funcnvuni  7954  fiunlem  7964  frxp  8149  xporderlem  8150  poxp  8151  fnwelem  8154  fnse  8156  xpord2lem  8165  poxp2  8166  xpord3lem  8172  poxp3  8173  soseq  8182  oacan  8584  omword  8606  oeword  8626  oeoa  8633  qsdisj  8832  wemapso2lem  9589  brwdom  9604  cantnflem1  9726  r0weon  10049  infxpen  10051  sornom  10314  fin1ai  10330  isfin5  10336  isfin6  10337  sdom2en01  10339  enfin2i  10358  enfin1ai  10421  isfin5-2  10428  fin1a2lem7  10443  fin1a2lem11  10447  fin1a2lem13  10449  axdc3lem2  10488  engch  10665  eltskg  10787  tsken  10791  ltsonq  11006  addcanpr  11083  ltsosr  11131  axpre-lttri  11202  lemul1  12116  mulge0b  12135  mulle0b  12136  mulsuble0b  12137  nn1m1nn  12284  avgle  12505  nn0sub  12573  elznn0  12625  elz2  12628  nneo  12699  uztric  12899  mul2lt0bi  13138  ltxr  13154  xrrebnd  13206  xmulval  13263  xmulneg1  13307  ixxun  13399  iccsplit  13521  fzsplit2  13585  uzsplit  13632  nelfzo  13700  fzospliti  13727  fzouzsplit  13730  sqeqor  14251  swrdnd  14688  sumeq1  15721  sumeq2w  15724  sumeq2ii  15725  sumeq2sdv  15735  fz1f1o  15742  summo  15749  fsum  15752  prodeq1f  15938  prodeq1  15939  prodeq2w  15942  prodeq2ii  15943  prodeq2sdv  15955  prodmo  15968  fprod  15973  ruclem12  16273  odd2np1lem  16373  dvdsprime  16720  coprm  16744  vdwapun  17007  vdwlem6  17019  vdwlem10  17023  mreexexlemd  17688  mreexexd  17692  istos  18475  tosso  18476  tleile  18478  tsrlin  18642  tsrss  18646  islring  20556  isdomn  20721  prmirredlem  21500  domnchr  21564  zntoslem  21592  znfld  21596  fctop  23026  cctop  23028  ppttop  23029  pptbas  23030  isufil  23926  ufilss  23928  fixufil  23945  fin1aufil  23955  xpsdsval  24406  nlmmul0or  24719  pmltpclem1  25496  iundisj2  25597  mbfmax  25697  dvne0  26064  fta1glem2  26222  plymul0or  26336  ofmulrt  26337  quotval  26348  plydivlem3  26351  plydivlem4  26352  plydivex  26353  plydivalg  26355  quotlem  26356  aalioulem2  26389  quad2  26896  dcubic2  26901  dcubic  26903  dquartlem1  26908  dquart  26910  quart  26918  leibpilem2  26998  wilthlem1  27125  muval2  27191  perfectlem2  27288  lgslem1  27355  pntpbnd1  27644  slelss  27960  abssor  28284  n0s0suc  28359  n0s0m1  28373  elzn0s  28398  elzs2  28399  n0seo  28419  zseo  28420  legtrid  28613  legso  28621  ishlg  28624  lnhl  28637  symquadlem  28711  islmib  28809  isinag  28860  isinagd  28861  inaghl  28867  brbtwn2  28934  axcontlem2  28994  axcontlem4  28996  axcontlem11  29003  edglnl  29174  nb3grprlem2  29412  hashecclwwlkn1  30105  nfrgr2v  30300  h1datom  31610  atss  32374  atom1d  32381  atord  32416  chirred  32423  elimifd  32563  disji2f  32596  disjif2  32600  disjxpin  32607  iundisj2f  32609  disjunsn  32613  brprop  32711  quad3d  32760  fzsplit3  32801  iundisj2fi  32804  f1ocnt  32809  resstos  32941  trleile  32945  subrdom  33268  isprmidl  33445  prmidlc  33455  qsidomlem1  33459  qsidomlem2  33460  mxidlmax  33472  rprmval  33523  isrprm  33524  smatrcl  33756  fsumcvg4  33910  erdsze2lem2  35188  satf  35337  satfv1  35347  satfbrsuc  35350  satfrnmapom  35354  satf0op  35361  sat1el2xp  35363  fmlafvel  35369  fmlasuc  35370  fmla1  35371  isfmlasuc  35372  fmlaomn0  35374  fmlasucdisj  35383  satffunlem1lem1  35386  satffunlem1lem2  35387  satffunlem2lem1  35388  dmopab3rexdif  35389  satffunlem2lem2  35390  satfv1fvfmla1  35407  2goelgoanfmla1  35408  satefvfmla1  35409  funpsstri  35746  seglelin  36097  lineunray  36128  prodeq12sdv  36200  cbvsumdavw  36261  cbvproddavw  36262  cbvsumdavw2  36277  cbvproddavw2  36278  weiunlem1  36444  topdifinffinlem  37329  topdifinffin  37330  topdifinfeq  37332  mblfinlem2  37644  itg2addnclem2  37658  iblabsnclem  37669  ftc1anclem5  37683  fdc1  37732  unichnidl  38017  ispridl  38020  maxidlmax  38029  disjressuc2  38369  qsdisjALTV  38596  lcvexchlem4  39018  lcvexchlem5  39019  2at0mat0  39507  pmapjoin  39834  cdlemg17h  40650  dihlspsnat  41315  lzunuz  42755  dvdsrabdioph  42797  acongeq12d  42967  jm2.25  42987  rmydioph  43002  expdioph  43011  fnwe2val  43037  aomclem8  43049  fzunt  43444  fzuntd  43445  fzunt1d  43446  fzuntgd  43447  sqrtcvallem1  43620  brfvrcld2  43681  uneqsn  44014  ntrneixb  44084  ntrneix3  44086  ntrneix13  44088  mnringmulrcld  44223  disjinfi  45134  salexct  46289  salexct2  46294  salexct3  46297  salgencntex  46298  salgensscntex  46299  nnfoctbdjlem  46410  nnfoctbdj  46411  iundjiun  46415  opprb  46980  euoreqb  47058  el1fzopredsuc  47274  iccpartgel  47353  paireqne  47435  divgcdoddALTV  47606  perfectALTVlem2  47646  clnbgrel  47752  dfvopnbgr2  47776  vopnbgrel  47777  dfclnbgr6  47779  dfnbgr6  47780  clnbgrgrim  47839  gpg5nbgrvtx03starlem1  47958  gpg5nbgrvtx03starlem2  47959  gpg5nbgrvtx03starlem3  47960  gpg5nbgrvtx13starlem1  47961  gpg5nbgrvtx13starlem2  47962  gpg5nbgrvtx13starlem3  47963  lindslinindsimp2lem5  48307  ldepspr  48318  rrx2pnedifcoorneor  48565  rrx2plord  48569  rrx2plordisom  48572  itsclc0yqsol  48613