Theorem orbi12d 916

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 914	. 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜃)))
3		bi12d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	3	orbi2d 913	. 2 ⊢ (𝜑 → ((𝜒 ∨ 𝜃) ↔ (𝜒 ∨ 𝜏)))
5	2, 4	bitrd 278	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜏)))

Syntax hints:   → wi 4   ↔ wb 205   ∨ wo 844

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 206  df-or 845

This theorem is referenced by:  pm4.39  974  ifpbi123d  1077  ifpbi123dOLD  1078  3orbi123d  1434  cadbi123d  1612  eueq3  3647  sbcor  3770  unjust  3892  elun  4084  elprg  4583  eltpg  4622  reuprg0  4639  rabsnifsb  4659  rabrsn  4661  preq12bg  4785  uniprg  4857  disji2  5057  disjprgw  5070  disjprg  5071  disjxun  5073  swopolem  5514  sotrieq  5533  isso2i  5539  dmopab2rex  5829  somin1  6043  ordequn  6370  fununi  6516  unima  6852  unpreima  6949  ordsucun  7681  funcnvuni  7787  fiunlem  7793  frxp  7976  xporderlem  7977  poxp  7978  fnwelem  7981  fnse  7983  oacan  8388  omword  8410  oeword  8430  oeoa  8437  qsdisj  8592  wemapso2lem  9320  brwdom  9335  cantnflem1  9456  r0weon  9777  infxpen  9779  sornom  10042  fin1ai  10058  isfin5  10064  isfin6  10065  sdom2en01  10067  enfin2i  10086  enfin1ai  10149  isfin5-2  10156  fin1a2lem7  10171  fin1a2lem11  10175  fin1a2lem13  10177  axdc3lem2  10216  engch  10393  eltskg  10515  tsken  10519  ltsonq  10734  addcanpr  10811  ltsosr  10859  axpre-lttri  10930  lemul1  11836  mulge0b  11854  mulle0b  11855  mulsuble0b  11856  nn1m1nn  12003  avgle  12224  nn0sub  12292  elznn0  12343  elz2  12346  nneo  12413  uztric  12615  mul2lt0bi  12845  ltxr  12860  xrrebnd  12911  xmulval  12968  xmulneg1  13012  ixxun  13104  iccsplit  13226  fzsplit2  13290  uzsplit  13337  nelfzo  13401  fzospliti  13428  fzouzsplit  13431  sqeqor  13941  swrdnd  14376  sumeq1  15409  sumeq2w  15413  sumeq2ii  15414  fz1f1o  15431  summo  15438  fsum  15441  prodeq1f  15627  prodeq2w  15631  prodeq2ii  15632  prodmo  15655  fprod  15660  ruclem12  15959  odd2np1lem  16058  dvdsprime  16401  coprm  16425  vdwapun  16684  vdwlem6  16696  vdwlem10  16700  mreexexlemd  17362  mreexexd  17366  istos  18145  tosso  18146  tleile  18148  tsrlin  18312  tsrss  18316  isdomn  20574  prmirredlem  20703  domnchr  20745  zntoslem  20773  znfld  20777  fctop  22163  cctop  22165  ppttop  22166  pptbas  22167  isufil  23063  ufilss  23065  fixufil  23082  fin1aufil  23092  xpsdsval  23543  nlmmul0or  23856  pmltpclem1  24621  iundisj2  24722  mbfmax  24822  dvne0  25184  fta1glem2  25340  plymul0or  25450  ofmulrt  25451  quotval  25461  plydivlem3  25464  plydivlem4  25465  plydivex  25466  plydivalg  25468  quotlem  25469  aalioulem2  25502  quad2  25998  dcubic2  26003  dcubic  26005  dquartlem1  26010  dquart  26012  quart  26020  leibpilem2  26100  wilthlem1  26226  muval2  26292  perfectlem2  26387  lgslem1  26454  pntpbnd1  26743  legtrid  26961  legso  26969  ishlg  26972  lnhl  26985  symquadlem  27059  islmib  27157  isinag  27208  isinagd  27209  inaghl  27215  brbtwn2  27282  axcontlem2  27342  axcontlem4  27344  axcontlem11  27351  edglnl  27522  nb3grprlem2  27757  hashecclwwlkn1  28450  nfrgr2v  28645  h1datom  29953  atss  30717  atom1d  30724  atord  30759  chirred  30766  elimifd  30895  disji2f  30925  disjif2  30929  disjxpin  30936  iundisj2f  30938  disjunsn  30942  brprop  31039  fzsplit3  31124  iundisj2fi  31127  f1ocnt  31132  resstos  31254  trleile  31258  isprmidl  31622  prmidlc  31633  qsidomlem1  31637  qsidomlem2  31638  mxidlmax  31646  rprmval  31673  isrprm  31674  smatrcl  31755  fsumcvg4  31909  erdsze2lem2  33175  satf  33324  satfv1  33334  satfbrsuc  33337  satfrnmapom  33341  satf0op  33348  sat1el2xp  33350  fmlafvel  33356  fmlasuc  33357  fmla1  33358  isfmlasuc  33359  fmlaomn0  33361  fmlasucdisj  33370  satffunlem1lem1  33373  satffunlem1lem2  33374  satffunlem2lem1  33375  dmopab3rexdif  33376  satffunlem2lem2  33377  satfv1fvfmla1  33394  2goelgoanfmla1  33395  satefvfmla1  33396  eqfunresadj  33744  funpsstri  33748  xpord2lem  33798  poxp2  33799  xpord3lem  33804  poxp3  33805  soseq  33812  seglelin  34427  lineunray  34458  topdifinffinlem  35527  topdifinffin  35528  topdifinfeq  35530  mblfinlem2  35824  itg2addnclem2  35838  iblabsnclem  35849  ftc1anclem5  35863  fdc1  35913  unichnidl  36198  ispridl  36201  maxidlmax  36210  qsdisjALTV  36735  lcvexchlem4  37058  lcvexchlem5  37059  2at0mat0  37546  pmapjoin  37873  cdlemg17h  38689  dihlspsnat  39354  lzunuz  40597  dvdsrabdioph  40639  acongeq12d  40808  jm2.25  40828  rmydioph  40843  expdioph  40852  fnwe2val  40881  aomclem8  40893  fzunt  41069  fzuntd  41070  fzunt1d  41071  fzuntgd  41072  sqrtcvallem1  41246  brfvrcld2  41307  uneqsn  41640  ntrneixb  41712  ntrneix3  41714  ntrneix13  41716  mnringmulrcld  41853  disjinfi  42738  salexct  43880  salexct2  43885  salexct3  43888  salgencntex  43889  salgensscntex  43890  nnfoctbdjlem  44000  nnfoctbdj  44001  iundjiun  44005  opprb  44536  euoreqb  44612  el1fzopredsuc  44828  iccpartgel  44892  paireqne  44974  divgcdoddALTV  45145  perfectALTVlem2  45185  lindslinindsimp2lem5  45814  ldepspr  45825  rrx2pnedifcoorneor  46073  rrx2plord  46077  rrx2plordisom  46080  itsclc0yqsol  46121