Theorem orbi12d 932

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  pm4.39  992  ifpbi123d  1095  3orbi123d  1463  cadbi123d  1643  eueq3  3669  sbcor  3789  unjust  3903  elun  4100  elprg  4607  eltpg  4647  el7g  4651  reuprg0  4663  rabsnifsb  4683  rabrsn  4685  preq12bg  4813  uniprg  4883  disji2  5087  disjprg  5099  disjxun  5101  axprg  5395  swopolem  5569  sotrieq  5590  isso2i  5596  dmopab2rex  5899  somin1  6127  ordequn  6467  fununi  6613  unima  6958  unpreima  7060  eqfunresadj  7368  ordsucun  7834  funcnvuni  7942  fiunlem  7952  frxp  8136  xporderlem  8137  poxp  8138  fnwelem  8141  fnse  8143  xpord2lem  8152  poxp2  8153  xpord3lem  8159  poxp3  8160  soseq  8169  oacan  8549  omword  8571  oeword  8592  oeoa  8599  qsdisj  8808  wemapso2lem  9539  brwdom  9554  cantnflem1  9683  r0weon  10084  infxpen  10086  sornom  10348  fin1ai  10364  isfin5  10370  isfin6  10371  sdom2en01  10373  enfin2i  10392  enfin1ai  10455  isfin5-2  10462  fin1a2lem7  10477  fin1a2lem11  10481  fin1a2lem13  10483  axdc3lem2  10522  engch  10706  eltskg  10828  tsken  10832  ltsonq  11047  addcanpr  11124  ltsosr  11172  axpre-lttri  11243  lemul1  12162  mulge0b  12180  mulle0b  12181  mulsuble0b  12182  nn1m1nn  12349  avgle  12581  nn0sub  12649  elznn0  12701  elz2  12704  nneo  12776  uztric  12982  mul2lt0bi  13221  ltxr  13237  xrrebnd  13291  xmulval  13348  xmulneg1  13392  ixxun  13485  iccsplit  13609  fzsplit2  13676  uzsplit  13723  nelfzo  13792  fzospliti  13819  fzouzsplit  13822  sqeqor  14353  swrdnd  14797  sumeq1  15849  sumeq2w  15852  sumeq2ii  15853  sumeq2sdv  15863  fz1f1o  15869  summo  15876  fsum  15879  prodeq1f  16068  prodeq1  16069  prodeq2w  16072  prodeq2ii  16073  prodeq2sdv  16084  prodmo  16096  fprod  16101  ruclem12  16402  odd2np1lem  16503  dvdsprime  16855  coprm  16880  vdwapun  17145  vdwlem6  17157  vdwlem10  17161  mreexexlemd  17811  mreexexd  17815  istos  18583  tosso  18584  tleile  18586  resstos  18597  tsrlin  18752  tsrss  18756  islring  20785  isdomn  20950  unichnlidl  21509  isprmidl  21612  prmidlc  21622  qsidomlem1  21629  qsidomlem2  21630  prmirredlem  21771  domnchr  21831  zntoslem  21855  znfld  21859  fctop  23315  cctop  23317  ppttop  23318  pptbas  23319  isufil  24215  ufilss  24217  fixufil  24234  fin1aufil  24244  xpsdsval  24693  nlmmul0or  24995  pmltpclem1  25762  iundisj2  25863  mbfmax  25963  dvne0  26324  fta1glem2  26480  plymul0or  26592  ofmulrt  26593  quotval  26606  plydivlem3  26609  plydivlem4  26610  plydivex  26611  plydivalg  26613  quotlem  26614  aalioulem2  26653  quad2  27160  dcubic2  27165  dcubic  27167  dquartlem1  27172  dquart  27174  quart  27182  leibpilem2  27262  wilthlem1  27388  muval2  27454  perfectlem2  27550  lgslem1  27617  pntpbnd1  27906  leslss  28288  abssor  28625  n0s0suc  28721  n0s0m1  28741  nn1m1nns  28753  elzn0s  28777  elzs2  28778  zsoring  28788  n0seo  28800  zseo  28801  bdayfinbndcbv  28845  bdayfinbndlem1  28846  bdayfinbndlem2  28847  bdayfinbnd  28848  z12zsodd  28861  legtrid  29047  legso  29055  ishlg2  29058  ishlg  29061  lnhl  29074  symquadlem  29154  plngcplem  29256  islmib  29285  isinag  29350  isinagd  29351  inaghl  29357  brprlng  29409  brbtwn2  29476  axcontlem2  29536  axcontlem4  29538  axcontlem11  29545  edglnl  29714  nb3grprlem2  29955  hashecclwwlkn1  30661  nfrgr2v  30866  h1datom  32177  atss  32941  atom1d  32948  atord  32983  chirred  32990  elimifd  33132  disji2f  33164  disjif2  33168  disjxpin  33175  iundisj2f  33177  disjunsn  33181  brprop  33283  quad3d  33334  fzsplit3  33378  iundisj2fi  33382  f1ocnt  33385  trleile  33525  domnpropd  33834  subrdom  33839  mxidlmax  33983  rprmval  34041  isrprm  34042  smatrcl  34421  fsumcvg4  34575  erdsze2lem2  35948  satf  36097  satfv1  36107  satfbrsuc  36110  satfrnmapom  36114  satf0op  36121  sat1el2xp  36123  fmlafvel  36129  fmlasuc  36130  fmla1  36131  isfmlasuc  36132  fmlaomn0  36134  fmlasucdisj  36143  satffunlem1lem1  36146  satffunlem1lem2  36147  satffunlem2lem1  36148  dmopab3rexdif  36149  satffunlem2lem2  36150  satfv1fvfmla1  36167  2goelgoanfmla1  36168  satefvfmla1  36169  funpsstri  36510  seglelin  36861  lineunray  36892  ltnadd  36947  naddle  36948  prodeq12sdv  36987  cbvsumdavw  37048  cbvproddavw  37049  cbvsumdavw2  37064  cbvproddavw2  37065  weiunval  37230  axtcond  37246  topdifinffinlem  38250  topdifinffin  38251  topdifinfeq  38253  mblfinlem2  38556  itg2addnclem2  38570  iblabsnclem  38581  ftc1anclem5  38595  fdc1  38660  unichnidl  38945  ispridl  38948  maxidlmax  38957  disjressuc2  39323  qsdisjALTV  39611  lcvexchlem4  40074  lcvexchlem5  40075  2at0mat0  40562  pmapjoin  40889  cdlemg17h  41705  dihlspsnat  42370  quadfac  43235  lzunuz  43758  dvdsrabdioph  43796  acongeq12d  43965  jm2.25  43985  rmydioph  44000  expdioph  44009  fnwe2val  44035  aomclem8  44047  fzunt  44440  fzuntd  44441  fzunt1d  44442  fzuntgd  44443  sqrtcvallem1  44616  brfvrcld2  44677  uneqsn  45010  ntrneixb  45080  ntrneix3  45082  ntrneix13  45084  mnringmulrcld  45211  disjinfi  46176  salexct  47313  salexct2  47318  salexct3  47321  salgencntex  47322  salgensscntex  47323  nnfoctbdjlem  47434  nnfoctbdj  47435  iundjiun  47439  opprb  48070  euoreqb  48148  el1fzopredsuc  48365  iccpartgel  48480  paireqne  48562  divgcdoddALTV  48749  perfectALTVlem2  48789  clnbgrel  48895  dfvopnbgr2  48920  vopnbgrel  48921  dfclnbgr6  48923  dfnbgr6  48924  clnbgrgrim  49001  gpg5nbgrvtx03starlem1  49135  gpg5nbgrvtx03starlem2  49136  gpg5nbgrvtx03starlem3  49137  gpg5nbgrvtx13starlem1  49138  gpg5nbgrvtx13starlem2  49139  gpg5nbgrvtx13starlem3  49140  gpg5edgnedg  49197  lindslinindsimp2lem5  49543  ldepspr  49554  rrx2pnedifcoorneor  49797  rrx2plord  49801  rrx2plordisom  49804  itsclc0yqsol  49845