Theorem orbi12d 917

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

Syntax hints:   → wi 4   ↔ wb 205   ∨ wo 846

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 206  df-or 847

This theorem is referenced by:  pm4.39  975  ifpbi123d  1077  3orbi123d  1432  cadbi123d  1604  eueq3  3704  sbcor  3827  unjust  3948  elun  4144  elprg  4645  eltpg  4685  reuprg0  4702  rabsnifsb  4722  rabrsn  4724  preq12bg  4850  uniprg  4919  disji2  5124  disjprgw  5137  disjprg  5138  disjxun  5140  swopolem  5594  sotrieq  5613  isso2i  5619  dmopab2rex  5914  somin1  6133  ordequn  6466  fununi  6622  unima  6967  unpreima  7066  eqfunresadj  7362  ordsucun  7822  funcnvuni  7933  fiunlem  7939  frxp  8125  xporderlem  8126  poxp  8127  fnwelem  8130  fnse  8132  xpord2lem  8141  poxp2  8142  xpord3lem  8148  poxp3  8149  soseq  8158  oacan  8562  omword  8584  oeword  8604  oeoa  8611  qsdisj  8806  wemapso2lem  9569  brwdom  9584  cantnflem1  9706  r0weon  10029  infxpen  10031  sornom  10294  fin1ai  10310  isfin5  10316  isfin6  10317  sdom2en01  10319  enfin2i  10338  enfin1ai  10401  isfin5-2  10408  fin1a2lem7  10423  fin1a2lem11  10427  fin1a2lem13  10429  axdc3lem2  10468  engch  10645  eltskg  10767  tsken  10771  ltsonq  10986  addcanpr  11063  ltsosr  11111  axpre-lttri  11182  lemul1  12090  mulge0b  12108  mulle0b  12109  mulsuble0b  12110  nn1m1nn  12257  avgle  12478  nn0sub  12546  elznn0  12597  elz2  12600  nneo  12670  uztric  12870  mul2lt0bi  13106  ltxr  13121  xrrebnd  13173  xmulval  13230  xmulneg1  13274  ixxun  13366  iccsplit  13488  fzsplit2  13552  uzsplit  13599  nelfzo  13663  fzospliti  13690  fzouzsplit  13693  sqeqor  14205  swrdnd  14630  sumeq1  15661  sumeq2w  15664  sumeq2ii  15665  fz1f1o  15682  summo  15689  fsum  15692  prodeq1f  15878  prodeq2w  15882  prodeq2ii  15883  prodmo  15906  fprod  15911  ruclem12  16211  odd2np1lem  16310  dvdsprime  16651  coprm  16675  vdwapun  16936  vdwlem6  16948  vdwlem10  16952  mreexexlemd  17617  mreexexd  17621  istos  18403  tosso  18404  tleile  18406  tsrlin  18570  tsrss  18574  islring  20470  isdomn  21234  prmirredlem  21391  domnchr  21455  zntoslem  21483  znfld  21487  fctop  22900  cctop  22902  ppttop  22903  pptbas  22904  isufil  23800  ufilss  23802  fixufil  23819  fin1aufil  23829  xpsdsval  24280  nlmmul0or  24593  pmltpclem1  25370  iundisj2  25471  mbfmax  25571  dvne0  25937  fta1glem2  26096  plymul0or  26208  ofmulrt  26209  quotval  26220  plydivlem3  26223  plydivlem4  26224  plydivex  26225  plydivalg  26227  quotlem  26228  aalioulem2  26261  quad2  26764  dcubic2  26769  dcubic  26771  dquartlem1  26776  dquart  26778  quart  26786  leibpilem2  26866  wilthlem1  26993  muval2  27059  perfectlem2  27156  lgslem1  27223  pntpbnd1  27512  slelss  27827  abssor  28133  legtrid  28388  legso  28396  ishlg  28399  lnhl  28412  symquadlem  28486  islmib  28584  isinag  28635  isinagd  28636  inaghl  28642  brbtwn2  28709  axcontlem2  28769  axcontlem4  28771  axcontlem11  28778  edglnl  28949  nb3grprlem2  29187  hashecclwwlkn1  29880  nfrgr2v  30075  h1datom  31385  atss  32149  atom1d  32156  atord  32191  chirred  32198  elimifd  32327  disji2f  32360  disjif2  32364  disjxpin  32371  iundisj2f  32373  disjunsn  32377  brprop  32471  fzsplit3  32556  iundisj2fi  32559  f1ocnt  32564  resstos  32688  trleile  32692  isprmidl  33143  prmidlc  33154  qsidomlem1  33158  qsidomlem2  33159  mxidlmax  33168  rprmval  33220  isrprm  33221  smatrcl  33387  fsumcvg4  33541  erdsze2lem2  34804  satf  34953  satfv1  34963  satfbrsuc  34966  satfrnmapom  34970  satf0op  34977  sat1el2xp  34979  fmlafvel  34985  fmlasuc  34986  fmla1  34987  isfmlasuc  34988  fmlaomn0  34990  fmlasucdisj  34999  satffunlem1lem1  35002  satffunlem1lem2  35003  satffunlem2lem1  35004  dmopab3rexdif  35005  satffunlem2lem2  35006  satfv1fvfmla1  35023  2goelgoanfmla1  35024  satefvfmla1  35025  funpsstri  35351  seglelin  35702  lineunray  35733  topdifinffinlem  36816  topdifinffin  36817  topdifinfeq  36819  mblfinlem2  37120  itg2addnclem2  37134  iblabsnclem  37145  ftc1anclem5  37159  fdc1  37208  unichnidl  37493  ispridl  37496  maxidlmax  37505  disjressuc2  37849  qsdisjALTV  38076  lcvexchlem4  38498  lcvexchlem5  38499  2at0mat0  38987  pmapjoin  39314  cdlemg17h  40130  dihlspsnat  40795  lzunuz  42160  dvdsrabdioph  42202  acongeq12d  42372  jm2.25  42392  rmydioph  42407  expdioph  42416  fnwe2val  42445  aomclem8  42457  fzunt  42857  fzuntd  42858  fzunt1d  42859  fzuntgd  42860  sqrtcvallem1  43033  brfvrcld2  43094  uneqsn  43427  ntrneixb  43497  ntrneix3  43499  ntrneix13  43501  mnringmulrcld  43637  disjinfi  44537  salexct  45694  salexct2  45699  salexct3  45702  salgencntex  45703  salgensscntex  45704  nnfoctbdjlem  45815  nnfoctbdj  45816  iundjiun  45820  opprb  46385  euoreqb  46461  el1fzopredsuc  46677  iccpartgel  46741  paireqne  46823  divgcdoddALTV  46994  perfectALTVlem2  47034  lindslinindsimp2lem5  47502  ldepspr  47513  rrx2pnedifcoorneor  47761  rrx2plord  47765  rrx2plordisom  47768  itsclc0yqsol  47809