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  5402  swopolem  5573  sotrieq  5594  isso2i  5600  dmopab2rex  5901  somin1  6127  ordequn  6463  fununi  6608  unima  6953  unpreima  7055  eqfunresadj  7363  ordsucun  7821  funcnvuni  7929  fiunlem  7939  frxp  8124  xporderlem  8125  poxp  8126  fnwelem  8129  fnse  8131  xpord2lem  8140  poxp2  8141  xpord3lem  8147  poxp3  8148  soseq  8157  oacan  8535  omword  8557  oeword  8578  oeoa  8585  qsdisj  8794  wemapso2lem  9524  brwdom  9539  cantnflem1  9668  r0weon  10015  infxpen  10017  sornom  10279  fin1ai  10295  isfin5  10301  isfin6  10302  sdom2en01  10304  enfin2i  10323  enfin1ai  10386  isfin5-2  10393  fin1a2lem7  10408  fin1a2lem11  10412  fin1a2lem13  10414  axdc3lem2  10453  engch  10637  eltskg  10759  tsken  10763  ltsonq  10978  addcanpr  11055  ltsosr  11103  axpre-lttri  11174  lemul1  12091  mulge0b  12109  mulle0b  12110  mulsuble0b  12111  nn1m1nn  12278  avgle  12510  nn0sub  12578  elznn0  12630  elz2  12633  nneo  12705  uztric  12911  mul2lt0bi  13150  ltxr  13166  xrrebnd  13220  xmulval  13277  xmulneg1  13321  ixxun  13414  iccsplit  13538  fzsplit2  13604  uzsplit  13651  nelfzo  13720  fzospliti  13747  fzouzsplit  13750  sqeqor  14280  swrdnd  14724  sumeq1  15776  sumeq2w  15779  sumeq2ii  15780  sumeq2sdv  15790  fz1f1o  15796  summo  15803  fsum  15806  prodeq1f  15995  prodeq1  15996  prodeq2w  15999  prodeq2ii  16000  prodeq2sdv  16011  prodmo  16023  fprod  16028  ruclem12  16329  odd2np1lem  16430  dvdsprime  16777  coprm  16802  vdwapun  17066  vdwlem6  17078  vdwlem10  17082  mreexexlemd  17732  mreexexd  17736  istos  18504  tosso  18505  tleile  18507  resstos  18518  tsrlin  18673  tsrss  18677  islring  20702  isdomn  20867  unichnlidl  21425  isprmidl  21526  prmidlc  21536  qsidomlem1  21543  qsidomlem2  21544  prmirredlem  21685  domnchr  21745  zntoslem  21769  znfld  21773  fctop  23229  cctop  23231  ppttop  23232  pptbas  23233  isufil  24129  ufilss  24131  fixufil  24148  fin1aufil  24158  xpsdsval  24607  nlmmul0or  24909  pmltpclem1  25676  iundisj2  25777  mbfmax  25877  dvne0  26238  fta1glem2  26394  plymul0or  26508  ofmulrt  26509  quotval  26522  plydivlem3  26525  plydivlem4  26526  plydivex  26527  plydivalg  26529  quotlem  26530  aalioulem2  26569  quad2  27076  dcubic2  27081  dcubic  27083  dquartlem1  27088  dquart  27090  quart  27098  leibpilem2  27178  wilthlem1  27304  muval2  27370  perfectlem2  27466  lgslem1  27533  pntpbnd1  27822  leslss  28174  abssor  28511  n0s0suc  28607  n0s0m1  28627  nn1m1nns  28639  elzn0s  28663  elzs2  28664  zsoring  28674  n0seo  28686  zseo  28687  bdayfinbndcbv  28731  bdayfinbndlem1  28732  bdayfinbndlem2  28733  bdayfinbnd  28734  z12zsodd  28747  legtrid  28933  legso  28941  ishlg2  28944  ishlg  28947  lnhl  28960  symquadlem  29040  plngcplem  29142  islmib  29171  isinag  29236  isinagd  29237  inaghl  29243  brprlng  29295  brbtwn2  29362  axcontlem2  29422  axcontlem4  29424  axcontlem11  29431  edglnl  29600  nb3grprlem2  29841  hashecclwwlkn1  30547  nfrgr2v  30752  h1datom  32063  atss  32827  atom1d  32834  atord  32869  chirred  32876  elimifd  33018  disji2f  33050  disjif2  33054  disjxpin  33061  iundisj2f  33063  disjunsn  33067  brprop  33169  quad3d  33220  fzsplit3  33264  iundisj2fi  33268  f1ocnt  33271  trleile  33411  domnpropd  33720  subrdom  33725  mxidlmax  33868  rprmval  33926  isrprm  33927  smatrcl  34306  fsumcvg4  34460  erdsze2lem2  35783  satf  35932  satfv1  35942  satfbrsuc  35945  satfrnmapom  35949  satf0op  35956  sat1el2xp  35958  fmlafvel  35964  fmlasuc  35965  fmla1  35966  isfmlasuc  35967  fmlaomn0  35969  fmlasucdisj  35978  satffunlem1lem1  35981  satffunlem1lem2  35982  satffunlem2lem1  35983  dmopab3rexdif  35984  satffunlem2lem2  35985  satfv1fvfmla1  36002  2goelgoanfmla1  36003  satefvfmla1  36004  funpsstri  36345  seglelin  36696  lineunray  36727  ltnadd  36798  naddle  36799  prodeq12sdv  36838  cbvsumdavw  36899  cbvproddavw  36900  cbvsumdavw2  36915  cbvproddavw2  36916  weiunval  37081  axtcond  37097  topdifinffinlem  38101  topdifinffin  38102  topdifinfeq  38104  mblfinlem2  38407  itg2addnclem2  38421  iblabsnclem  38432  ftc1anclem5  38446  fdc1  38496  unichnidl  38781  ispridl  38784  maxidlmax  38793  disjressuc2  39159  qsdisjALTV  39447  lcvexchlem4  39910  lcvexchlem5  39911  2at0mat0  40398  pmapjoin  40725  cdlemg17h  41541  dihlspsnat  42206  quadfac  43071  lzunuz  43613  dvdsrabdioph  43651  acongeq12d  43820  jm2.25  43840  rmydioph  43855  expdioph  43864  fnwe2val  43890  aomclem8  43902  fzunt  44295  fzuntd  44296  fzunt1d  44297  fzuntgd  44298  sqrtcvallem1  44471  brfvrcld2  44532  uneqsn  44865  ntrneixb  44935  ntrneix3  44937  ntrneix13  44939  mnringmulrcld  45066  disjinfi  46024  salexct  47162  salexct2  47167  salexct3  47170  salgencntex  47171  salgensscntex  47172  nnfoctbdjlem  47283  nnfoctbdj  47284  iundjiun  47288  opprb  47919  euoreqb  47997  el1fzopredsuc  48214  iccpartgel  48329  paireqne  48411  divgcdoddALTV  48598  perfectALTVlem2  48638  clnbgrel  48744  dfvopnbgr2  48769  vopnbgrel  48770  dfclnbgr6  48772  dfnbgr6  48773  clnbgrgrim  48850  gpg5nbgrvtx03starlem1  48984  gpg5nbgrvtx03starlem2  48985  gpg5nbgrvtx03starlem3  48986  gpg5nbgrvtx13starlem1  48987  gpg5nbgrvtx13starlem2  48988  gpg5nbgrvtx13starlem3  48989  gpg5edgnedg  49046  lindslinindsimp2lem5  49392  ldepspr  49403  rrx2pnedifcoorneor  49646  rrx2plord  49650  rrx2plordisom  49653  itsclc0yqsol  49694