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  3667  sbcor  3789  unjust  3903  elun  4104  elprg  4600  eltpg  4640  el7g  4644  reuprg0  4656  rabsnifsb  4676  rabrsn  4678  preq12bg  4806  uniprg  4876  disji2  5079  disjprg  5091  disjxun  5093  swopolem  5539  sotrieq  5560  isso2i  5566  dmopab2rex  5864  somin1  6087  ordequn  6419  fununi  6564  unima  6906  unpreima  7005  eqfunresadj  7303  ordsucun  7764  funcnvuni  7871  fiunlem  7883  frxp  8065  xporderlem  8066  poxp  8067  fnwelem  8070  fnse  8072  xpord2lem  8081  poxp2  8082  xpord3lem  8088  poxp3  8089  soseq  8098  oacan  8472  omword  8494  oeword  8514  oeoa  8521  qsdisj  8727  wemapso2lem  9448  brwdom  9463  cantnflem1  9589  r0weon  9913  infxpen  9915  sornom  10178  fin1ai  10194  isfin5  10200  isfin6  10201  sdom2en01  10203  enfin2i  10222  enfin1ai  10285  isfin5-2  10292  fin1a2lem7  10307  fin1a2lem11  10311  fin1a2lem13  10313  axdc3lem2  10352  engch  10529  eltskg  10651  tsken  10655  ltsonq  10870  addcanpr  10947  ltsosr  10995  axpre-lttri  11066  lemul1  11983  mulge0b  12002  mulle0b  12003  mulsuble0b  12004  nn1m1nn  12156  avgle  12373  nn0sub  12441  elznn0  12493  elz2  12496  nneo  12567  uztric  12766  mul2lt0bi  13008  ltxr  13024  xrrebnd  13077  xmulval  13134  xmulneg1  13178  ixxun  13271  iccsplit  13395  fzsplit2  13459  uzsplit  13506  nelfzo  13574  fzospliti  13601  fzouzsplit  13604  sqeqor  14133  swrdnd  14572  sumeq1  15606  sumeq2w  15609  sumeq2ii  15610  sumeq2sdv  15620  fz1f1o  15627  summo  15634  fsum  15637  prodeq1f  15823  prodeq1  15824  prodeq2w  15827  prodeq2ii  15828  prodeq2sdv  15840  prodmo  15853  fprod  15858  ruclem12  16160  odd2np1lem  16261  dvdsprime  16608  coprm  16632  vdwapun  16896  vdwlem6  16908  vdwlem10  16912  mreexexlemd  17560  mreexexd  17564  istos  18332  tosso  18333  tleile  18335  resstos  18346  tsrlin  18501  tsrss  18505  islring  20465  isdomn  20630  prmirredlem  21419  domnchr  21479  zntoslem  21503  znfld  21507  fctop  22929  cctop  22931  ppttop  22932  pptbas  22933  isufil  23828  ufilss  23830  fixufil  23847  fin1aufil  23857  xpsdsval  24306  nlmmul0or  24608  pmltpclem1  25386  iundisj2  25487  mbfmax  25587  dvne0  25953  fta1glem2  26111  plymul0or  26225  ofmulrt  26226  quotval  26237  plydivlem3  26240  plydivlem4  26241  plydivex  26242  plydivalg  26244  quotlem  26245  aalioulem2  26278  quad2  26786  dcubic2  26791  dcubic  26793  dquartlem1  26798  dquart  26800  quart  26808  leibpilem2  26888  wilthlem1  27015  muval2  27081  perfectlem2  27178  lgslem1  27245  pntpbnd1  27534  slelss  27864  abssor  28194  n0s0suc  28280  n0s0m1  28298  nn1m1nns  28309  elzn0s  28332  elzs2  28333  zsoring  28342  n0seo  28354  zseo  28355  zs12zodd  28402  legtrid  28579  legso  28587  ishlg  28590  lnhl  28603  symquadlem  28677  islmib  28775  isinag  28826  isinagd  28827  inaghl  28833  brbtwn2  28894  axcontlem2  28954  axcontlem4  28956  axcontlem11  28963  edglnl  29132  nb3grprlem2  29370  hashecclwwlkn1  30068  nfrgr2v  30263  h1datom  31573  atss  32337  atom1d  32344  atord  32379  chirred  32386  elimifd  32534  disji2f  32568  disjif2  32572  disjxpin  32579  iundisj2f  32581  disjunsn  32585  brprop  32689  quad3d  32744  fzsplit3  32787  iundisj2fi  32790  f1ocnt  32793  trleile  32963  domnpropd  33254  subrdom  33262  isprmidl  33414  prmidlc  33424  qsidomlem1  33428  qsidomlem2  33429  mxidlmax  33441  rprmval  33492  isrprm  33493  smatrcl  33820  fsumcvg4  33974  erdsze2lem2  35259  satf  35408  satfv1  35418  satfbrsuc  35421  satfrnmapom  35425  satf0op  35432  sat1el2xp  35434  fmlafvel  35440  fmlasuc  35441  fmla1  35442  isfmlasuc  35443  fmlaomn0  35445  fmlasucdisj  35454  satffunlem1lem1  35457  satffunlem1lem2  35458  satffunlem2lem1  35459  dmopab3rexdif  35460  satffunlem2lem2  35461  satfv1fvfmla1  35478  2goelgoanfmla1  35479  satefvfmla1  35480  funpsstri  35821  seglelin  36171  lineunray  36202  prodeq12sdv  36273  cbvsumdavw  36334  cbvproddavw  36335  cbvsumdavw2  36350  cbvproddavw2  36351  weiunlem1  36517  topdifinffinlem  37402  topdifinffin  37403  topdifinfeq  37405  mblfinlem2  37708  itg2addnclem2  37722  iblabsnclem  37733  ftc1anclem5  37747  fdc1  37796  unichnidl  38081  ispridl  38084  maxidlmax  38093  disjressuc2  38445  qsdisjALTV  38721  lcvexchlem4  39146  lcvexchlem5  39147  2at0mat0  39634  pmapjoin  39961  cdlemg17h  40777  dihlspsnat  41442  lzunuz  42875  dvdsrabdioph  42917  acongeq12d  43086  jm2.25  43106  rmydioph  43121  expdioph  43130  fnwe2val  43156  aomclem8  43168  fzunt  43562  fzuntd  43563  fzunt1d  43564  fzuntgd  43565  sqrtcvallem1  43738  brfvrcld2  43799  uneqsn  44132  ntrneixb  44202  ntrneix3  44204  ntrneix13  44206  mnringmulrcld  44335  disjinfi  45303  salexct  46446  salexct2  46451  salexct3  46454  salgencntex  46455  salgensscntex  46456  nnfoctbdjlem  46567  nnfoctbdj  46568  iundjiun  46572  opprb  47145  euoreqb  47223  el1fzopredsuc  47439  iccpartgel  47543  paireqne  47625  divgcdoddALTV  47796  perfectALTVlem2  47836  clnbgrel  47942  dfvopnbgr2  47967  vopnbgrel  47968  dfclnbgr6  47970  dfnbgr6  47971  clnbgrgrim  48048  gpg5nbgrvtx03starlem1  48182  gpg5nbgrvtx03starlem2  48183  gpg5nbgrvtx03starlem3  48184  gpg5nbgrvtx13starlem1  48185  gpg5nbgrvtx13starlem2  48186  gpg5nbgrvtx13starlem3  48187  gpg5edgnedg  48244  lindslinindsimp2lem5  48577  ldepspr  48588  rrx2pnedifcoorneor  48831  rrx2plord  48835  rrx2plordisom  48838  itsclc0yqsol  48879