Theorem oveq12i 7374

Description: Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)

Hypotheses

Ref	Expression
oveq1i.1	⊢ 𝐴 = 𝐵
oveq12i.2	⊢ 𝐶 = 𝐷

Assertion

Ref	Expression
oveq12i	⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐷)

Proof of Theorem oveq12i

Step	Hyp	Ref	Expression
1		oveq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		oveq12i.2	. 2 ⊢ 𝐶 = 𝐷
3		oveq12 7371	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
4	1, 2, 3	mp2an 693	1 ⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐷)

Syntax hints:   = wceq 1542  (class class class)co 7362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6450  df-fv 6502  df-ov 7365

This theorem is referenced by:  oveq123i  7376  caovdir  7596  caovdilem  7597  caovlem2  7598  cnfcom2  9618  canthwelem  10568  adderpqlem  10872  addassnq  10876  distrnq  10879  ltanq  10889  1lt2nq  10891  ltexnq  10893  halfnq  10894  mulcmpblnrlem  10988  mulcomsr  11007  distrsr  11009  m1p1sr  11010  m1m1sr  11011  mulgt0sr  11023  addcnsrec  11061  mulcnsrec  11062  axmulcom  11073  axmulass  11075  axdistr  11076  axi2m1  11077  addrid  11321  3t3e9  12338  8th4div3  12392  halfthird  12393  numma  12683  decmul10add  12708  4t3lem  12736  9t11e99  12769  5recm6rec  12782  fz0to3un2pr  13578  seqfeq4  14008  seqof  14016  sqdivi  14142  sq4e2t8  14156  i4  14161  binom2i  14169  nn0opthlem1  14225  facp1  14235  fac2  14236  fac3  14237  fac4  14238  faclbnd4lem1  14250  4bc2eq6  14286  ccat2s1len  14581  ccat2s1p2  14588  cats1len  14817  cats2cat  14819  ofs2  14928  cji  15116  01sqrexlem5  15203  fsumadd  15697  fsumsplitf  15699  fsumsplitsnun  15712  0.999...  15841  fprodmul  15920  fproddiv  15921  fprodsplitf  15948  bpoly3  16018  fsumcube  16020  efsep  16072  ef01bndlem  16146  cos2bnd  16150  rpnnen2lem3  16178  3dvds2dec  16297  flodddiv4  16379  sadeq  16436  gcdaddmlem  16488  bezout  16507  nn0expgcd  16528  nn0gcdsq  16717  pythagtriplem16  16796  4sqlem19  16929  dec5nprm  17032  dec2nprm  17033  mod2xnegi  17037  numexp2x  17044  decsplit  17048  karatsuba  17049  2exp5  17051  2exp11  17055  2exp16  17056  37prm  17086  43prm  17087  83prm  17088  139prm  17089  163prm  17090  317prm  17091  631prm  17092  1259lem1  17096  1259lem2  17097  1259lem3  17098  1259lem4  17099  1259lem5  17100  1259prm  17101  2503lem1  17102  2503lem2  17103  2503lem3  17104  2503prm  17105  4001lem1  17106  4001lem2  17107  4001lem3  17108  4001lem4  17109  4001prm  17110  funcoppc  17837  estrchom  18088  funcestrcsetclem5  18105  yonedalem3b  18240  ecqusaddd  19162  symgressbas  19352  gsum2dlem2  19941  gsumle  20115  opprrng  20320  isrhm  20453  rngqiprnglinlem2  21286  pzriprng1ALT  21490  evlsval  22078  mamudi  22382  mamudir  22383  oftpos  22431  mamutpos  22437  mdetrlin  22581  mdetrlin2  22586  mdetunilem5  22595  cpmadugsumfi  22856  cnmpt2res  23656  ussval  24238  icopnfhmeo  24924  iccpnfhmeo  24926  pcoass  25005  ovolunlem1a  25477  ioombl1lem3  25541  ioombl1lem4  25542  mbfimaopnlem  25636  itgfsum  25808  iblabslem  25809  itgsplit  25817  dveflem  25960  efhalfpi  26452  efipi  26454  sin2pi  26456  ef2pi  26458  sincosq3sgn  26481  sincosq4sgn  26482  sinq34lt0t  26490  sincos4thpi  26494  tan4thpi  26495  tan4thpiOLD  26496  sincos6thpi  26497  sincos3rdpi  26498  pigt3  26499  pige3ALT  26501  cxpcn3  26729  lawcos  26797  1cubrlem  26822  quart1lem  26836  quart1  26837  asin1  26875  atancj  26891  atanlogsublem  26896  log2cnv  26925  log2tlbnd  26926  log2ublem3  26929  log2ub  26930  birthday  26935  basellem8  27069  basellem9  27070  cht2  27153  cht3  27154  1sgm2ppw  27181  bclbnd  27261  bposlem8  27272  bposlem9  27273  lgsdi  27315  lgsquadlem1  27361  2lgsoddprmlem3c  27393  2lgsoddprmlem3d  27394  addsqnreup  27424  addsval2  27973  addsunif  28012  addsasslem1  28013  addsasslem2  28014  negsval  28035  neg0s  28036  neg1s  28037  negsid  28051  mulsval2  28121  muls01  28122  mulsproplem2  28127  mulsproplem3  28128  mulsproplem4  28129  mulsproplem5  28130  mulsproplem6  28131  mulsproplem7  28132  mulsproplem8  28133  mulsproplem12  28137  mulsproplem13  28138  mulsproplem14  28139  mulsunif  28160  addsdilem1  28161  addsdilem2  28162  mulsasslem1  28173  mulsasslem2  28174  mulsunif2  28180  precsexlem11  28227  onmulscl  28288  twocut  28433  mirauto  28770  axsegconlem9  29012  ax5seglem7  29022  vtxdginducedm1  29631  clwlkclwwlkfo  30098  eupth2eucrct  30306  ex-exp  30539  ex-fac  30540  ex-bc  30541  ex-hash  30542  ip0i  30915  ip1ilem  30916  ip2i  30918  ipdirilem  30919  ipasslem10  30929  ip2dii  30934  pythi  30940  siilem1  30941  hvsubsub4i  31149  hvsubcan2i  31154  hisubcomi  31194  normlem0  31199  normlem1  31200  normlem2  31201  normlem3  31202  normlem6  31205  normlem8  31207  normlem9  31208  bcseqi  31210  norm-ii-i  31227  norm-iii-i  31229  normpythi  31232  norm3difi  31237  normpari  31244  normpar2i  31246  polid2i  31247  polidi  31248  bcsiALT  31269  lediri  31627  h1de2i  31643  cmcmlem  31681  cmbr2i  31686  cm2j  31710  fh3i  31713  fh4i  31714  pjaddii  31765  pjsslem  31769  pjssmii  31771  pjdifnormii  31773  lnopeq0lem1  32095  lnopunilem1  32100  lnophmlem2  32107  pjsdi2i  32247  pjclem1  32285  golem1  32361  dpmul100  32975  dpmul1000  32977  dpadd2  32988  dpadd  32989  dpadd3  32990  dpmul  32991  dpmul4  32992  ccatws1f1o  33030  elrgspnlem2  33323  matdim  33779  fldext2chn  33892  constrextdg2lem  33912  constrext2chnlem  33914  iconstr  33930  cos9thpiminplylem4  33949  cos9thpiminplylem5  33950  rmulccn  34092  raddcn  34093  xrmulc1cn  34094  xrge0iifhmeo  34100  qqh0  34148  qqh1  34149  elmbfmvol2  34431  mbfmcnt  34432  eulerpartlemgvv  34540  eulerpartlemgh  34542  fib2  34566  fib3  34567  fib4  34568  fib5  34569  fib6  34570  ballotlem2  34653  ballotlemfval0  34660  ballotth  34702  hgt750lem2  34816  problem2  35868  problem4  35870  quad3  35872  ditgeq123i  36411  cbvditgvw2  36451  poimirlem30  37989  iblabsnclem  38022  dalem10  40137  cdleme0e  40681  cdleme7c  40709  cdleme20c  40775  3exp7  42510  3lexlogpow5ineq1  42511  3lexlogpow5ineq5  42517  aks4d1p1  42533  5bc2eq10  42599  aks5lem3a  42646  sn-1ne2  42721  sqmid3api  42733  sqdeccom12  42739  sq3deccom12  42740  tan3rdpi  42802  sin2t3rdpi  42803  cos2t3rdpi  42804  rei4  42874  ipiiie0  42888  sn-0tie0  42914  mzpcompact2lem  43201  pellexlem5  43283  pellfundgt1  43333  jm2.27c  43457  areaquad  43666  resqrtvalex  44094  imsqrtvalex  44095  lhe4.4ex1a  44778  mccl  46050  dvnprodlem2  46397  itgsin0pilem1  46400  stoweidlem13  46463  wallispilem4  46518  wallispi2lem1  46521  wallispi2lem2  46522  dirkerper  46546  dirkertrigeqlem1  46548  fourierdlem30  46587  fourierdlem47  46603  fourierdlem103  46659  fourierdlem104  46660  fouriersw  46681  etransclem37  46721  sge0splitmpt  46861  sge0xaddlem2  46884  sge0xadd  46885  caragen0  46956  caragenuncllem  46962  nthrucw  47336  goldrasin  47348  fsumsplitsndif  47845  139prmALT  48075  127prm  48078  m11nprm  48080  3exp4mod41  48095  ppivalnn4  48106  sbgoldbo  48279  2t6m3t4e0  48840  lincsum  48921  zlmodzxzequa  48988  zlmodzxzequap  48991  zlmodzxzldeplem3  48994  rrx2linest  49234  line2  49244  itsclc0yqsollem1  49254  itsclquadb  49268  itscnhlinecirc02plem2  49275  postcofval  49855  postcofcl  49856  precofval  49858  precofvalALT  49859  precofcl  49861  termcfuncval  50023