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  3694  sbcor  3816  unjust  3930  elun  4128  elprg  4624  eltpg  4662  el7g  4666  reuprg0  4678  rabsnifsb  4698  rabrsn  4700  preq12bg  4829  uniprg  4899  disji2  5103  disjprg  5115  disjxun  5117  swopolem  5571  sotrieq  5592  isso2i  5598  dmopab2rex  5897  somin1  6122  ordequn  6457  fununi  6611  unima  6954  unpreima  7053  eqfunresadj  7353  ordsucun  7819  funcnvuni  7928  fiunlem  7940  frxp  8125  xporderlem  8126  poxp  8127  fnwelem  8130  fnse  8132  xpord2lem  8141  poxp2  8142  xpord3lem  8148  poxp3  8149  soseq  8158  oacan  8560  omword  8582  oeword  8602  oeoa  8609  qsdisj  8808  wemapso2lem  9566  brwdom  9581  cantnflem1  9703  r0weon  10026  infxpen  10028  sornom  10291  fin1ai  10307  isfin5  10313  isfin6  10314  sdom2en01  10316  enfin2i  10335  enfin1ai  10398  isfin5-2  10405  fin1a2lem7  10420  fin1a2lem11  10424  fin1a2lem13  10426  axdc3lem2  10465  engch  10642  eltskg  10764  tsken  10768  ltsonq  10983  addcanpr  11060  ltsosr  11108  axpre-lttri  11179  lemul1  12093  mulge0b  12112  mulle0b  12113  mulsuble0b  12114  nn1m1nn  12261  avgle  12483  nn0sub  12551  elznn0  12603  elz2  12606  nneo  12677  uztric  12876  mul2lt0bi  13115  ltxr  13131  xrrebnd  13184  xmulval  13241  xmulneg1  13285  ixxun  13378  iccsplit  13502  fzsplit2  13566  uzsplit  13613  nelfzo  13681  fzospliti  13708  fzouzsplit  13711  sqeqor  14234  swrdnd  14672  sumeq1  15705  sumeq2w  15708  sumeq2ii  15709  sumeq2sdv  15719  fz1f1o  15726  summo  15733  fsum  15736  prodeq1f  15922  prodeq1  15923  prodeq2w  15926  prodeq2ii  15927  prodeq2sdv  15939  prodmo  15952  fprod  15957  ruclem12  16259  odd2np1lem  16359  dvdsprime  16706  coprm  16730  vdwapun  16994  vdwlem6  17006  vdwlem10  17010  mreexexlemd  17656  mreexexd  17660  istos  18428  tosso  18429  tleile  18431  tsrlin  18595  tsrss  18599  islring  20500  isdomn  20665  prmirredlem  21433  domnchr  21493  zntoslem  21517  znfld  21521  fctop  22942  cctop  22944  ppttop  22945  pptbas  22946  isufil  23841  ufilss  23843  fixufil  23860  fin1aufil  23870  xpsdsval  24320  nlmmul0or  24622  pmltpclem1  25401  iundisj2  25502  mbfmax  25602  dvne0  25968  fta1glem2  26126  plymul0or  26240  ofmulrt  26241  quotval  26252  plydivlem3  26255  plydivlem4  26256  plydivex  26257  plydivalg  26259  quotlem  26260  aalioulem2  26293  quad2  26801  dcubic2  26806  dcubic  26808  dquartlem1  26813  dquart  26815  quart  26823  leibpilem2  26903  wilthlem1  27030  muval2  27096  perfectlem2  27193  lgslem1  27260  pntpbnd1  27549  slelss  27872  abssor  28200  n0s0suc  28286  n0s0m1  28304  nn1m1nns  28315  elzn0s  28338  elzs2  28339  n0seo  28359  zseo  28360  legtrid  28570  legso  28578  ishlg  28581  lnhl  28594  symquadlem  28668  islmib  28766  isinag  28817  isinagd  28818  inaghl  28824  brbtwn2  28884  axcontlem2  28944  axcontlem4  28946  axcontlem11  28953  edglnl  29122  nb3grprlem2  29360  hashecclwwlkn1  30058  nfrgr2v  30253  h1datom  31563  atss  32327  atom1d  32334  atord  32369  chirred  32376  elimifd  32524  disji2f  32558  disjif2  32562  disjxpin  32569  iundisj2f  32571  disjunsn  32575  brprop  32674  quad3d  32727  fzsplit3  32770  iundisj2fi  32774  f1ocnt  32779  resstos  32947  trleile  32951  domnpropd  33271  subrdom  33279  isprmidl  33453  prmidlc  33463  qsidomlem1  33467  qsidomlem2  33468  mxidlmax  33480  rprmval  33531  isrprm  33532  smatrcl  33827  fsumcvg4  33981  erdsze2lem2  35226  satf  35375  satfv1  35385  satfbrsuc  35388  satfrnmapom  35392  satf0op  35399  sat1el2xp  35401  fmlafvel  35407  fmlasuc  35408  fmla1  35409  isfmlasuc  35410  fmlaomn0  35412  fmlasucdisj  35421  satffunlem1lem1  35424  satffunlem1lem2  35425  satffunlem2lem1  35426  dmopab3rexdif  35427  satffunlem2lem2  35428  satfv1fvfmla1  35445  2goelgoanfmla1  35446  satefvfmla1  35447  funpsstri  35783  seglelin  36134  lineunray  36165  prodeq12sdv  36236  cbvsumdavw  36297  cbvproddavw  36298  cbvsumdavw2  36313  cbvproddavw2  36314  weiunlem1  36480  topdifinffinlem  37365  topdifinffin  37366  topdifinfeq  37368  mblfinlem2  37682  itg2addnclem2  37696  iblabsnclem  37707  ftc1anclem5  37721  fdc1  37770  unichnidl  38055  ispridl  38058  maxidlmax  38067  disjressuc2  38406  qsdisjALTV  38633  lcvexchlem4  39055  lcvexchlem5  39056  2at0mat0  39544  pmapjoin  39871  cdlemg17h  40687  dihlspsnat  41352  lzunuz  42791  dvdsrabdioph  42833  acongeq12d  43003  jm2.25  43023  rmydioph  43038  expdioph  43047  fnwe2val  43073  aomclem8  43085  fzunt  43479  fzuntd  43480  fzunt1d  43481  fzuntgd  43482  sqrtcvallem1  43655  brfvrcld2  43716  uneqsn  44049  ntrneixb  44119  ntrneix3  44121  ntrneix13  44123  mnringmulrcld  44252  disjinfi  45216  salexct  46363  salexct2  46368  salexct3  46371  salgencntex  46372  salgensscntex  46373  nnfoctbdjlem  46484  nnfoctbdj  46485  iundjiun  46489  opprb  47060  euoreqb  47138  el1fzopredsuc  47354  iccpartgel  47443  paireqne  47525  divgcdoddALTV  47696  perfectALTVlem2  47736  clnbgrel  47842  dfvopnbgr2  47866  vopnbgrel  47867  dfclnbgr6  47869  dfnbgr6  47870  clnbgrgrim  47947  gpg5nbgrvtx03starlem1  48070  gpg5nbgrvtx03starlem2  48071  gpg5nbgrvtx03starlem3  48072  gpg5nbgrvtx13starlem1  48073  gpg5nbgrvtx13starlem2  48074  gpg5nbgrvtx13starlem3  48075  lindslinindsimp2lem5  48438  ldepspr  48449  rrx2pnedifcoorneor  48696  rrx2plord  48700  rrx2plordisom  48703  itsclc0yqsol  48744