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  1610  eueq3  3685  sbcor  3807  unjust  3921  elun  4119  elprg  4615  eltpg  4653  el7g  4657  reuprg0  4669  rabsnifsb  4689  rabrsn  4691  preq12bg  4820  uniprg  4890  disji2  5094  disjprg  5106  disjxun  5108  swopolem  5559  sotrieq  5580  isso2i  5586  dmopab2rex  5884  somin1  6109  ordequn  6440  fununi  6594  unima  6939  unpreima  7038  eqfunresadj  7338  ordsucun  7803  funcnvuni  7911  fiunlem  7923  frxp  8108  xporderlem  8109  poxp  8110  fnwelem  8113  fnse  8115  xpord2lem  8124  poxp2  8125  xpord3lem  8131  poxp3  8132  soseq  8141  oacan  8515  omword  8537  oeword  8557  oeoa  8564  qsdisj  8770  wemapso2lem  9512  brwdom  9527  cantnflem1  9649  r0weon  9972  infxpen  9974  sornom  10237  fin1ai  10253  isfin5  10259  isfin6  10260  sdom2en01  10262  enfin2i  10281  enfin1ai  10344  isfin5-2  10351  fin1a2lem7  10366  fin1a2lem11  10370  fin1a2lem13  10372  axdc3lem2  10411  engch  10588  eltskg  10710  tsken  10714  ltsonq  10929  addcanpr  11006  ltsosr  11054  axpre-lttri  11125  lemul1  12041  mulge0b  12060  mulle0b  12061  mulsuble0b  12062  nn1m1nn  12214  avgle  12431  nn0sub  12499  elznn0  12551  elz2  12554  nneo  12625  uztric  12824  mul2lt0bi  13066  ltxr  13082  xrrebnd  13135  xmulval  13192  xmulneg1  13236  ixxun  13329  iccsplit  13453  fzsplit2  13517  uzsplit  13564  nelfzo  13632  fzospliti  13659  fzouzsplit  13662  sqeqor  14188  swrdnd  14626  sumeq1  15662  sumeq2w  15665  sumeq2ii  15666  sumeq2sdv  15676  fz1f1o  15683  summo  15690  fsum  15693  prodeq1f  15879  prodeq1  15880  prodeq2w  15883  prodeq2ii  15884  prodeq2sdv  15896  prodmo  15909  fprod  15914  ruclem12  16216  odd2np1lem  16317  dvdsprime  16664  coprm  16688  vdwapun  16952  vdwlem6  16964  vdwlem10  16968  mreexexlemd  17612  mreexexd  17616  istos  18384  tosso  18385  tleile  18387  tsrlin  18551  tsrss  18555  islring  20456  isdomn  20621  prmirredlem  21389  domnchr  21449  zntoslem  21473  znfld  21477  fctop  22898  cctop  22900  ppttop  22901  pptbas  22902  isufil  23797  ufilss  23799  fixufil  23816  fin1aufil  23826  xpsdsval  24276  nlmmul0or  24578  pmltpclem1  25356  iundisj2  25457  mbfmax  25557  dvne0  25923  fta1glem2  26081  plymul0or  26195  ofmulrt  26196  quotval  26207  plydivlem3  26210  plydivlem4  26211  plydivex  26212  plydivalg  26214  quotlem  26215  aalioulem2  26248  quad2  26756  dcubic2  26761  dcubic  26763  dquartlem1  26768  dquart  26770  quart  26778  leibpilem2  26858  wilthlem1  26985  muval2  27051  perfectlem2  27148  lgslem1  27215  pntpbnd1  27504  slelss  27827  abssor  28155  n0s0suc  28241  n0s0m1  28259  nn1m1nns  28270  elzn0s  28293  elzs2  28294  n0seo  28314  zseo  28315  legtrid  28525  legso  28533  ishlg  28536  lnhl  28549  symquadlem  28623  islmib  28721  isinag  28772  isinagd  28773  inaghl  28779  brbtwn2  28839  axcontlem2  28899  axcontlem4  28901  axcontlem11  28908  edglnl  29077  nb3grprlem2  29315  hashecclwwlkn1  30013  nfrgr2v  30208  h1datom  31518  atss  32282  atom1d  32289  atord  32324  chirred  32331  elimifd  32479  disji2f  32513  disjif2  32517  disjxpin  32524  iundisj2f  32526  disjunsn  32530  brprop  32627  quad3d  32680  fzsplit3  32723  iundisj2fi  32727  f1ocnt  32732  resstos  32900  trleile  32904  domnpropd  33234  subrdom  33242  isprmidl  33416  prmidlc  33426  qsidomlem1  33430  qsidomlem2  33431  mxidlmax  33443  rprmval  33494  isrprm  33495  smatrcl  33793  fsumcvg4  33947  erdsze2lem2  35198  satf  35347  satfv1  35357  satfbrsuc  35360  satfrnmapom  35364  satf0op  35371  sat1el2xp  35373  fmlafvel  35379  fmlasuc  35380  fmla1  35381  isfmlasuc  35382  fmlaomn0  35384  fmlasucdisj  35393  satffunlem1lem1  35396  satffunlem1lem2  35397  satffunlem2lem1  35398  dmopab3rexdif  35399  satffunlem2lem2  35400  satfv1fvfmla1  35417  2goelgoanfmla1  35418  satefvfmla1  35419  funpsstri  35760  seglelin  36111  lineunray  36142  prodeq12sdv  36213  cbvsumdavw  36274  cbvproddavw  36275  cbvsumdavw2  36290  cbvproddavw2  36291  weiunlem1  36457  topdifinffinlem  37342  topdifinffin  37343  topdifinfeq  37345  mblfinlem2  37659  itg2addnclem2  37673  iblabsnclem  37684  ftc1anclem5  37698  fdc1  37747  unichnidl  38032  ispridl  38035  maxidlmax  38044  disjressuc2  38381  qsdisjALTV  38613  lcvexchlem4  39037  lcvexchlem5  39038  2at0mat0  39526  pmapjoin  39853  cdlemg17h  40669  dihlspsnat  41334  lzunuz  42763  dvdsrabdioph  42805  acongeq12d  42975  jm2.25  42995  rmydioph  43010  expdioph  43019  fnwe2val  43045  aomclem8  43057  fzunt  43451  fzuntd  43452  fzunt1d  43453  fzuntgd  43454  sqrtcvallem1  43627  brfvrcld2  43688  uneqsn  44021  ntrneixb  44091  ntrneix3  44093  ntrneix13  44095  mnringmulrcld  44224  disjinfi  45193  salexct  46339  salexct2  46344  salexct3  46347  salgencntex  46348  salgensscntex  46349  nnfoctbdjlem  46460  nnfoctbdj  46461  iundjiun  46465  opprb  47036  euoreqb  47114  el1fzopredsuc  47330  iccpartgel  47434  paireqne  47516  divgcdoddALTV  47687  perfectALTVlem2  47727  clnbgrel  47833  dfvopnbgr2  47857  vopnbgrel  47858  dfclnbgr6  47860  dfnbgr6  47861  clnbgrgrim  47938  gpg5nbgrvtx03starlem1  48063  gpg5nbgrvtx03starlem2  48064  gpg5nbgrvtx03starlem3  48065  gpg5nbgrvtx13starlem1  48066  gpg5nbgrvtx13starlem2  48067  gpg5nbgrvtx13starlem3  48068  lindslinindsimp2lem5  48455  ldepspr  48466  rrx2pnedifcoorneor  48709  rrx2plord  48713  rrx2plordisom  48716  itsclc0yqsol  48757