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  1611  eueq3  3670  sbcor  3792  unjust  3906  elun  4103  elprg  4599  eltpg  4639  el7g  4643  reuprg0  4655  rabsnifsb  4675  rabrsn  4677  preq12bg  4805  uniprg  4875  disji2  5075  disjprg  5087  disjxun  5089  swopolem  5534  sotrieq  5555  isso2i  5561  dmopab2rex  5857  somin1  6080  ordequn  6411  fununi  6556  unima  6897  unpreima  6996  eqfunresadj  7294  ordsucun  7755  funcnvuni  7862  fiunlem  7874  frxp  8056  xporderlem  8057  poxp  8058  fnwelem  8061  fnse  8063  xpord2lem  8072  poxp2  8073  xpord3lem  8079  poxp3  8080  soseq  8089  oacan  8463  omword  8485  oeword  8505  oeoa  8512  qsdisj  8718  wemapso2lem  9438  brwdom  9453  cantnflem1  9579  r0weon  9903  infxpen  9905  sornom  10168  fin1ai  10184  isfin5  10190  isfin6  10191  sdom2en01  10193  enfin2i  10212  enfin1ai  10275  isfin5-2  10282  fin1a2lem7  10297  fin1a2lem11  10301  fin1a2lem13  10303  axdc3lem2  10342  engch  10519  eltskg  10641  tsken  10645  ltsonq  10860  addcanpr  10937  ltsosr  10985  axpre-lttri  11056  lemul1  11973  mulge0b  11992  mulle0b  11993  mulsuble0b  11994  nn1m1nn  12146  avgle  12363  nn0sub  12431  elznn0  12483  elz2  12486  nneo  12557  uztric  12756  mul2lt0bi  12998  ltxr  13014  xrrebnd  13067  xmulval  13124  xmulneg1  13168  ixxun  13261  iccsplit  13385  fzsplit2  13449  uzsplit  13496  nelfzo  13564  fzospliti  13591  fzouzsplit  13594  sqeqor  14123  swrdnd  14562  sumeq1  15596  sumeq2w  15599  sumeq2ii  15600  sumeq2sdv  15610  fz1f1o  15617  summo  15624  fsum  15627  prodeq1f  15813  prodeq1  15814  prodeq2w  15817  prodeq2ii  15818  prodeq2sdv  15830  prodmo  15843  fprod  15848  ruclem12  16150  odd2np1lem  16251  dvdsprime  16598  coprm  16622  vdwapun  16886  vdwlem6  16898  vdwlem10  16902  mreexexlemd  17550  mreexexd  17554  istos  18322  tosso  18323  tleile  18325  resstos  18336  tsrlin  18491  tsrss  18495  islring  20456  isdomn  20621  prmirredlem  21410  domnchr  21470  zntoslem  21494  znfld  21498  fctop  22920  cctop  22922  ppttop  22923  pptbas  22924  isufil  23819  ufilss  23821  fixufil  23838  fin1aufil  23848  xpsdsval  24297  nlmmul0or  24599  pmltpclem1  25377  iundisj2  25478  mbfmax  25578  dvne0  25944  fta1glem2  26102  plymul0or  26216  ofmulrt  26217  quotval  26228  plydivlem3  26231  plydivlem4  26232  plydivex  26233  plydivalg  26235  quotlem  26236  aalioulem2  26269  quad2  26777  dcubic2  26782  dcubic  26784  dquartlem1  26789  dquart  26791  quart  26799  leibpilem2  26879  wilthlem1  27006  muval2  27072  perfectlem2  27169  lgslem1  27236  pntpbnd1  27525  slelss  27855  abssor  28185  n0s0suc  28271  n0s0m1  28289  nn1m1nns  28300  elzn0s  28323  elzs2  28324  zsoring  28333  n0seo  28345  zseo  28346  zs12zodd  28393  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  30055  nfrgr2v  30250  h1datom  31560  atss  32324  atom1d  32331  atord  32366  chirred  32373  elimifd  32521  disji2f  32555  disjif2  32559  disjxpin  32566  iundisj2f  32568  disjunsn  32572  brprop  32676  quad3d  32731  fzsplit3  32774  iundisj2fi  32777  f1ocnt  32780  trleile  32950  domnpropd  33241  subrdom  33249  isprmidl  33401  prmidlc  33411  qsidomlem1  33415  qsidomlem2  33416  mxidlmax  33428  rprmval  33479  isrprm  33480  smatrcl  33807  fsumcvg4  33961  erdsze2lem2  35246  satf  35395  satfv1  35405  satfbrsuc  35408  satfrnmapom  35412  satf0op  35419  sat1el2xp  35421  fmlafvel  35427  fmlasuc  35428  fmla1  35429  isfmlasuc  35430  fmlaomn0  35432  fmlasucdisj  35441  satffunlem1lem1  35444  satffunlem1lem2  35445  satffunlem2lem1  35446  dmopab3rexdif  35447  satffunlem2lem2  35448  satfv1fvfmla1  35465  2goelgoanfmla1  35466  satefvfmla1  35467  funpsstri  35808  seglelin  36156  lineunray  36187  prodeq12sdv  36258  cbvsumdavw  36319  cbvproddavw  36320  cbvsumdavw2  36335  cbvproddavw2  36336  weiunlem1  36502  topdifinffinlem  37387  topdifinffin  37388  topdifinfeq  37390  mblfinlem2  37704  itg2addnclem2  37718  iblabsnclem  37729  ftc1anclem5  37743  fdc1  37792  unichnidl  38077  ispridl  38080  maxidlmax  38089  disjressuc2  38426  qsdisjALTV  38658  lcvexchlem4  39082  lcvexchlem5  39083  2at0mat0  39570  pmapjoin  39897  cdlemg17h  40713  dihlspsnat  41378  lzunuz  42807  dvdsrabdioph  42849  acongeq12d  43018  jm2.25  43038  rmydioph  43053  expdioph  43062  fnwe2val  43088  aomclem8  43100  fzunt  43494  fzuntd  43495  fzunt1d  43496  fzuntgd  43497  sqrtcvallem1  43670  brfvrcld2  43731  uneqsn  44064  ntrneixb  44134  ntrneix3  44136  ntrneix13  44138  mnringmulrcld  44267  disjinfi  45235  salexct  46378  salexct2  46383  salexct3  46386  salgencntex  46387  salgensscntex  46388  nnfoctbdjlem  46499  nnfoctbdj  46500  iundjiun  46504  opprb  47068  euoreqb  47146  el1fzopredsuc  47362  iccpartgel  47466  paireqne  47548  divgcdoddALTV  47719  perfectALTVlem2  47759  clnbgrel  47865  dfvopnbgr2  47890  vopnbgrel  47891  dfclnbgr6  47893  dfnbgr6  47894  clnbgrgrim  47971  gpg5nbgrvtx03starlem1  48105  gpg5nbgrvtx03starlem2  48106  gpg5nbgrvtx03starlem3  48107  gpg5nbgrvtx13starlem1  48108  gpg5nbgrvtx13starlem2  48109  gpg5nbgrvtx13starlem3  48110  gpg5edgnedg  48167  lindslinindsimp2lem5  48500  ldepspr  48511  rrx2pnedifcoorneor  48754  rrx2plord  48758  rrx2plordisom  48761  itsclc0yqsol  48802