Theorem oveq12i 7372

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 7369	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
4	1, 2, 3	mp2an 693	1 ⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐷)

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

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 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6449  df-fv 6501  df-ov 7363

This theorem is referenced by:  oveq123i  7374  caovdir  7594  caovdilem  7595  caovlem2  7596  cnfcom2  9615  canthwelem  10565  adderpqlem  10869  addassnq  10873  distrnq  10876  ltanq  10886  1lt2nq  10888  ltexnq  10890  halfnq  10891  mulcmpblnrlem  10985  mulcomsr  11004  distrsr  11006  m1p1sr  11007  m1m1sr  11008  mulgt0sr  11020  addcnsrec  11058  mulcnsrec  11059  axmulcom  11070  axmulass  11072  axdistr  11073  axi2m1  11074  addrid  11317  3t3e9  12311  8th4div3  12365  halfthird  12366  numma  12655  decmul10add  12680  4t3lem  12708  9t11e99  12741  5recm6rec  12754  fz0to3un2pr  13549  seqfeq4  13978  seqof  13986  sqdivi  14112  sq4e2t8  14126  i4  14131  binom2i  14139  nn0opthlem1  14195  facp1  14205  fac2  14206  fac3  14207  fac4  14208  faclbnd4lem1  14220  4bc2eq6  14256  ccat2s1len  14551  ccat2s1p2  14558  cats1len  14787  cats2cat  14789  ofs2  14898  cji  15086  01sqrexlem5  15173  fsumadd  15667  fsumsplitf  15669  fsumsplitsnun  15682  0.999...  15808  fprodmul  15887  fproddiv  15888  fprodsplitf  15915  bpoly3  15985  fsumcube  15987  efsep  16039  ef01bndlem  16113  cos2bnd  16117  rpnnen2lem3  16145  3dvds2dec  16264  flodddiv4  16346  sadeq  16403  gcdaddmlem  16455  bezout  16474  nn0expgcd  16495  nn0gcdsq  16683  pythagtriplem16  16762  4sqlem19  16895  dec5nprm  16998  dec2nprm  16999  mod2xnegi  17003  numexp2x  17010  decsplit  17014  karatsuba  17015  2exp5  17017  2exp11  17021  2exp16  17022  37prm  17052  43prm  17053  83prm  17054  139prm  17055  163prm  17056  317prm  17057  631prm  17058  1259lem1  17062  1259lem2  17063  1259lem3  17064  1259lem4  17065  1259lem5  17066  1259prm  17067  2503lem1  17068  2503lem2  17069  2503lem3  17070  2503prm  17071  4001lem1  17072  4001lem2  17073  4001lem3  17074  4001lem4  17075  4001prm  17076  funcoppc  17803  estrchom  18054  funcestrcsetclem5  18071  yonedalem3b  18206  ecqusaddd  19125  symgressbas  19315  gsum2dlem2  19904  gsumle  20078  opprrng  20285  isrhm  20418  rngqiprnglinlem2  21251  pzriprng1ALT  21455  evlsval  22045  mamudi  22351  mamudir  22352  oftpos  22400  mamutpos  22406  mdetrlin  22550  mdetrlin2  22555  mdetunilem5  22564  cpmadugsumfi  22825  cnmpt2res  23625  ussval  24207  icopnfhmeo  24901  iccpnfhmeo  24903  pcoass  24984  ovolunlem1a  25457  ioombl1lem3  25521  ioombl1lem4  25522  mbfimaopnlem  25616  itgfsum  25788  iblabslem  25789  itgsplit  25797  dveflem  25943  efhalfpi  26440  efipi  26442  sin2pi  26444  ef2pi  26446  sincosq3sgn  26469  sincosq4sgn  26470  sinq34lt0t  26478  sincos4thpi  26482  tan4thpi  26483  tan4thpiOLD  26484  sincos6thpi  26485  sincos3rdpi  26486  pigt3  26487  pige3ALT  26489  cxpcn3  26718  lawcos  26786  1cubrlem  26811  quart1lem  26825  quart1  26826  asin1  26864  atancj  26880  atanlogsublem  26885  log2cnv  26914  log2tlbnd  26915  log2ublem3  26918  log2ub  26919  birthday  26924  basellem8  27058  basellem9  27059  cht2  27142  cht3  27143  1sgm2ppw  27171  bclbnd  27251  bposlem8  27262  bposlem9  27263  lgsdi  27305  lgsquadlem1  27351  2lgsoddprmlem3c  27383  2lgsoddprmlem3d  27384  addsqnreup  27414  addsval2  27963  addsunif  28002  addsasslem1  28003  addsasslem2  28004  negsval  28025  neg0s  28026  neg1s  28027  negsid  28041  mulsval2  28111  muls01  28112  mulsproplem2  28117  mulsproplem3  28118  mulsproplem4  28119  mulsproplem5  28120  mulsproplem6  28121  mulsproplem7  28122  mulsproplem8  28123  mulsproplem12  28127  mulsproplem13  28128  mulsproplem14  28129  mulsunif  28150  addsdilem1  28151  addsdilem2  28152  mulsasslem1  28163  mulsasslem2  28164  mulsunif2  28170  precsexlem11  28217  onmulscl  28278  twocut  28423  mirauto  28760  axsegconlem9  29002  ax5seglem7  29012  vtxdginducedm1  29621  clwlkclwwlkfo  30088  eupth2eucrct  30296  ex-exp  30529  ex-fac  30530  ex-bc  30531  ex-hash  30532  ip0i  30904  ip1ilem  30905  ip2i  30907  ipdirilem  30908  ipasslem10  30918  ip2dii  30923  pythi  30929  siilem1  30930  hvsubsub4i  31138  hvsubcan2i  31143  hisubcomi  31183  normlem0  31188  normlem1  31189  normlem2  31190  normlem3  31191  normlem6  31194  normlem8  31196  normlem9  31197  bcseqi  31199  norm-ii-i  31216  norm-iii-i  31218  normpythi  31221  norm3difi  31226  normpari  31233  normpar2i  31235  polid2i  31236  polidi  31237  bcsiALT  31258  lediri  31616  h1de2i  31632  cmcmlem  31670  cmbr2i  31675  cm2j  31699  fh3i  31702  fh4i  31703  pjaddii  31754  pjsslem  31758  pjssmii  31760  pjdifnormii  31762  lnopeq0lem1  32084  lnopunilem1  32089  lnophmlem2  32096  pjsdi2i  32236  pjclem1  32274  golem1  32350  dpmul100  32980  dpmul1000  32982  dpadd2  32993  dpadd  32994  dpadd3  32995  dpmul  32996  dpmul4  32997  ccatws1f1o  33035  elrgspnlem2  33327  matdim  33774  fldext2chn  33887  constrextdg2lem  33907  constrext2chnlem  33909  iconstr  33925  cos9thpiminplylem4  33944  cos9thpiminplylem5  33945  rmulccn  34087  raddcn  34088  xrmulc1cn  34089  xrge0iifhmeo  34095  qqh0  34143  qqh1  34144  elmbfmvol2  34426  mbfmcnt  34427  eulerpartlemgvv  34535  eulerpartlemgh  34537  fib2  34561  fib3  34562  fib4  34563  fib5  34564  fib6  34565  ballotlem2  34648  ballotlemfval0  34655  ballotth  34697  hgt750lem2  34811  problem2  35862  problem4  35864  quad3  35866  ditgeq123i  36405  cbvditgvw2  36445  poimirlem30  37853  iblabsnclem  37886  dalem10  40001  cdleme0e  40545  cdleme7c  40573  cdleme20c  40639  3exp7  42375  3lexlogpow5ineq1  42376  3lexlogpow5ineq5  42382  aks4d1p1  42398  5bc2eq10  42464  aks5lem3a  42511  sn-1ne2  42587  sqmid3api  42605  sqdeccom12  42611  sq3deccom12  42612  tan3rdpi  42674  sin2t3rdpi  42675  cos2t3rdpi  42676  rei4  42746  ipiiie0  42760  sn-0tie0  42773  mzpcompact2lem  43060  pellexlem5  43142  pellfundgt1  43192  jm2.27c  43316  areaquad  43525  resqrtvalex  43953  imsqrtvalex  43954  lhe4.4ex1a  44637  mccl  45911  dvnprodlem2  46258  itgsin0pilem1  46261  stoweidlem13  46324  wallispilem4  46379  wallispi2lem1  46382  wallispi2lem2  46383  dirkerper  46407  dirkertrigeqlem1  46409  fourierdlem30  46448  fourierdlem47  46464  fourierdlem103  46520  fourierdlem104  46521  fouriersw  46542  etransclem37  46582  sge0splitmpt  46722  sge0xaddlem2  46745  sge0xadd  46746  caragen0  46817  caragenuncllem  46823  nthrucw  47197  fsumsplitsndif  47686  139prmALT  47909  127prm  47912  m11nprm  47914  3exp4mod41  47929  sbgoldbo  48100  2t6m3t4e0  48661  lincsum  48742  zlmodzxzequa  48809  zlmodzxzequap  48812  zlmodzxzldeplem3  48815  rrx2linest  49055  line2  49065  itsclc0yqsollem1  49075  itsclquadb  49089  itscnhlinecirc02plem2  49096  postcofval  49676  postcofcl  49677  precofval  49679  precofvalALT  49680  precofcl  49682  termcfuncval  49844