Theorem orbi12d 915

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

Syntax hints:   → wi 4   ↔ wb 208   ∨ wo 843

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 209  df-or 844

This theorem is referenced by:  pm4.39  973  ifpbi123d  1072  ifpbi123dOLD  1073  3orbi123d  1431  cadbi123d  1607  eueq3  3701  sbcor  3821  unjust  3939  elun  4124  elprg  4587  eltpg  4622  reuprg0  4637  rabsnifsb  4657  rabrsn  4659  preq12bg  4783  disji2  5047  disjprgw  5060  disjprg  5061  disjxun  5063  swopolem  5482  sotrieq  5501  isso2i  5507  dmopab2rex  5785  somin1  5992  ordequn  6290  fununi  6428  unima  6738  unpreima  6832  ordsucun  7539  funcnvuni  7635  fiunlem  7642  frxp  7819  xporderlem  7820  poxp  7821  fnwelem  7824  fnse  7826  oacan  8173  omword  8195  oeword  8215  oeoa  8222  qsdisj  8373  wemapso2lem  9015  brwdom  9030  cantnflem1  9151  r0weon  9437  infxpen  9439  sornom  9698  fin1ai  9714  isfin5  9720  isfin6  9721  sdom2en01  9723  enfin2i  9742  enfin1ai  9805  isfin5-2  9812  fin1a2lem7  9827  fin1a2lem11  9831  fin1a2lem13  9833  axdc3lem2  9872  engch  10049  eltskg  10171  tsken  10175  ltsonq  10390  addcanpr  10467  ltsosr  10515  axpre-lttri  10586  lemul1  11491  mulge0b  11509  mulle0b  11510  mulsuble0b  11511  nn1m1nn  11657  avgle  11878  nn0sub  11946  elznn0  11995  elz2  11998  nneo  12065  uztric  12265  mul2lt0bi  12494  ltxr  12509  xrrebnd  12560  xmulval  12617  xmulneg1  12661  ixxun  12753  iccsplit  12870  fzsplit2  12931  uzsplit  12978  nelfzo  13042  fzospliti  13068  fzouzsplit  13071  sqeqor  13577  swrdnd  14015  sumeq1  15044  sumeq2w  15048  sumeq2ii  15049  fz1f1o  15066  summo  15073  fsum  15076  prodeq1f  15261  prodeq2w  15265  prodeq2ii  15266  prodmo  15289  fprod  15294  ruclem12  15593  odd2np1lem  15688  dvdsprime  16030  coprm  16054  vdwapun  16309  vdwlem6  16321  vdwlem10  16325  mreexexlemd  16914  mreexexd  16918  istos  17644  tosso  17645  tsrlin  17828  tsrss  17832  isdomn  20066  prmirredlem  20639  domnchr  20678  zntoslem  20702  znfld  20706  fctop  21611  cctop  21613  ppttop  21614  pptbas  21615  isufil  22510  ufilss  22512  fixufil  22529  fin1aufil  22539  xpsdsval  22990  nlmmul0or  23291  pmltpclem1  24048  iundisj2  24149  mbfmax  24249  dvne0  24607  fta1glem2  24759  plymul0or  24869  ofmulrt  24870  quotval  24880  plydivlem3  24883  plydivlem4  24884  plydivex  24885  plydivalg  24887  quotlem  24888  aalioulem2  24921  quad2  25416  dcubic2  25421  dcubic  25423  dquartlem1  25428  dquart  25430  quart  25438  leibpilem2  25518  wilthlem1  25644  muval2  25710  perfectlem2  25805  lgslem1  25872  pntpbnd1  26161  legtrid  26376  legso  26384  ishlg  26387  lnhl  26400  symquadlem  26474  islmib  26572  isinag  26623  isinagd  26624  inaghl  26630  brbtwn2  26690  axcontlem2  26750  axcontlem4  26752  axcontlem11  26759  edglnl  26927  nb3grprlem2  27162  hashecclwwlkn1  27855  nfrgr2v  28050  h1datom  29358  atss  30122  atom1d  30129  atord  30164  chirred  30171  elimifd  30297  disji2f  30326  disjif2  30330  disjxpin  30337  iundisj2f  30339  disjunsn  30343  brprop  30432  fzsplit3  30516  iundisj2fi  30519  f1ocnt  30524  resstos  30647  tleile  30648  trleile  30653  isprmidl  30955  prmidlc  30964  qsidomlem1  30965  qsidomlem2  30966  mxidlmax  30974  smatrcl  31061  fsumcvg4  31193  erdsze2lem2  32451  satf  32600  satfv1  32610  satfbrsuc  32613  satfrnmapom  32617  satf0op  32624  sat1el2xp  32626  fmlafvel  32632  fmlasuc  32633  fmla1  32634  isfmlasuc  32635  fmlaomn0  32637  fmlasucdisj  32646  satffunlem1lem1  32649  satffunlem1lem2  32650  satffunlem2lem1  32651  dmopab3rexdif  32652  satffunlem2lem2  32653  satfv1fvfmla1  32670  2goelgoanfmla1  32671  satefvfmla1  32672  eqfunresadj  33004  funpsstri  33008  soseq  33096  seglelin  33577  lineunray  33608  topdifinffinlem  34627  topdifinffin  34628  topdifinfeq  34630  mblfinlem2  34929  itg2addnclem2  34943  iblabsnclem  34954  ftc1anclem5  34970  fdc1  35020  unichnidl  35308  ispridl  35311  maxidlmax  35320  qsdisjALTV  35849  lcvexchlem4  36172  lcvexchlem5  36173  2at0mat0  36660  pmapjoin  36987  cdlemg17h  37803  dihlspsnat  38468  lzunuz  39363  dvdsrabdioph  39405  acongeq12d  39574  jm2.25  39594  rmydioph  39609  expdioph  39618  fnwe2val  39647  aomclem8  39659  brfvrcld2  40035  uneqsn  40371  ntrneixb  40443  ntrneix3  40445  ntrneix13  40447  disjinfi  41452  salexct  42616  salexct2  42621  salexct3  42624  salgencntex  42625  salgensscntex  42626  nnfoctbdjlem  42736  nnfoctbdj  42737  iundjiun  42741  opprb  43265  euoreqb  43307  el1fzopredsuc  43524  iccpartgel  43588  paireqne  43672  divgcdoddALTV  43846  perfectALTVlem2  43886  lindslinindsimp2lem5  44516  ldepspr  44527  rrx2pnedifcoorneor  44702  rrx2plord  44706  rrx2plordisom  44709  itsclc0yqsol  44750