Theorem oveq12i 7353

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

Syntax hints:   = wceq 1541  (class class class)co 7341

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3394  df-v 3436  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4282  df-if 4474  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-br 5090  df-iota 6433  df-fv 6485  df-ov 7344

This theorem is referenced by:  oveq123i  7355  caovdir  7575  caovdilem  7576  caovlem2  7577  cnfcom2  9587  canthwelem  10533  adderpqlem  10837  addassnq  10841  distrnq  10844  ltanq  10854  1lt2nq  10856  ltexnq  10858  halfnq  10859  mulcmpblnrlem  10953  mulcomsr  10972  distrsr  10974  m1p1sr  10975  m1m1sr  10976  mulgt0sr  10988  addcnsrec  11026  mulcnsrec  11027  axmulcom  11038  axmulass  11040  axdistr  11041  axi2m1  11042  addrid  11285  3t3e9  12279  8th4div3  12333  halfthird  12334  numma  12624  decmul10add  12649  4t3lem  12677  9t11e99  12710  5recm6rec  12723  fz0to3un2pr  13521  seqfeq4  13950  seqof  13958  sqdivi  14084  sq4e2t8  14098  i4  14103  binom2i  14111  nn0opthlem1  14167  facp1  14177  fac2  14178  fac3  14179  fac4  14180  faclbnd4lem1  14192  4bc2eq6  14228  ccat2s1len  14523  ccat2s1p2  14530  cats1len  14759  cats2cat  14761  ofs2  14870  cji  15058  01sqrexlem5  15145  fsumadd  15639  fsumsplitf  15641  fsumsplitsnun  15654  0.999...  15780  fprodmul  15859  fproddiv  15860  fprodsplitf  15887  bpoly3  15957  fsumcube  15959  efsep  16011  ef01bndlem  16085  cos2bnd  16089  rpnnen2lem3  16117  3dvds2dec  16236  flodddiv4  16318  sadeq  16375  gcdaddmlem  16427  bezout  16446  nn0expgcd  16467  nn0gcdsq  16655  pythagtriplem16  16734  4sqlem19  16867  dec5nprm  16970  dec2nprm  16971  mod2xnegi  16975  numexp2x  16982  decsplit  16986  karatsuba  16987  2exp5  16989  2exp11  16993  2exp16  16994  37prm  17024  43prm  17025  83prm  17026  139prm  17027  163prm  17028  317prm  17029  631prm  17030  1259lem1  17034  1259lem2  17035  1259lem3  17036  1259lem4  17037  1259lem5  17038  1259prm  17039  2503lem1  17040  2503lem2  17041  2503lem3  17042  2503prm  17043  4001lem1  17044  4001lem2  17045  4001lem3  17046  4001lem4  17047  4001prm  17048  funcoppc  17774  estrchom  18025  funcestrcsetclem5  18042  yonedalem3b  18177  ecqusaddd  19097  symgressbas  19287  gsum2dlem2  19876  gsumle  20050  opprrng  20256  isrhm  20389  rngqiprnglinlem2  21222  pzriprng1ALT  21426  evlsval  22014  mamudi  22311  mamudir  22312  oftpos  22360  mamutpos  22366  mdetrlin  22510  mdetrlin2  22515  mdetunilem5  22524  cpmadugsumfi  22785  cnmpt2res  23585  ussval  24167  icopnfhmeo  24861  iccpnfhmeo  24863  pcoass  24944  ovolunlem1a  25417  ioombl1lem3  25481  ioombl1lem4  25482  mbfimaopnlem  25576  itgfsum  25748  iblabslem  25749  itgsplit  25757  dveflem  25903  efhalfpi  26400  efipi  26402  sin2pi  26404  ef2pi  26406  sincosq3sgn  26429  sincosq4sgn  26430  sinq34lt0t  26438  sincos4thpi  26442  tan4thpi  26443  tan4thpiOLD  26444  sincos6thpi  26445  sincos3rdpi  26446  pigt3  26447  pige3ALT  26449  cxpcn3  26678  lawcos  26746  1cubrlem  26771  quart1lem  26785  quart1  26786  asin1  26824  atancj  26840  atanlogsublem  26845  log2cnv  26874  log2tlbnd  26875  log2ublem3  26878  log2ub  26879  birthday  26884  basellem8  27018  basellem9  27019  cht2  27102  cht3  27103  1sgm2ppw  27131  bclbnd  27211  bposlem8  27222  bposlem9  27223  lgsdi  27265  lgsquadlem1  27311  2lgsoddprmlem3c  27343  2lgsoddprmlem3d  27344  addsqnreup  27374  addsval2  27899  addsunif  27938  addsasslem1  27939  addsasslem2  27940  negsval  27960  negs0s  27961  negs1s  27962  negsid  27976  mulsval2  28043  muls01  28044  mulsproplem2  28049  mulsproplem3  28050  mulsproplem4  28051  mulsproplem5  28052  mulsproplem6  28053  mulsproplem7  28054  mulsproplem8  28055  mulsproplem12  28059  mulsproplem13  28060  mulsproplem14  28061  mulsunif  28082  addsdilem1  28083  addsdilem2  28084  mulsasslem1  28095  mulsasslem2  28096  mulsunif2  28102  precsexlem11  28148  onmulscl  28204  1p1e2s  28332  twocut  28339  0reno  28392  mirauto  28655  axsegconlem9  28896  ax5seglem7  28906  vtxdginducedm1  29515  clwlkclwwlkfo  29979  eupth2eucrct  30187  ex-exp  30420  ex-fac  30421  ex-bc  30422  ex-hash  30423  ip0i  30795  ip1ilem  30796  ip2i  30798  ipdirilem  30799  ipasslem10  30809  ip2dii  30814  pythi  30820  siilem1  30821  hvsubsub4i  31029  hvsubcan2i  31034  hisubcomi  31074  normlem0  31079  normlem1  31080  normlem2  31081  normlem3  31082  normlem6  31085  normlem8  31087  normlem9  31088  bcseqi  31090  norm-ii-i  31107  norm-iii-i  31109  normpythi  31112  norm3difi  31117  normpari  31124  normpar2i  31126  polid2i  31127  polidi  31128  bcsiALT  31149  lediri  31507  h1de2i  31523  cmcmlem  31561  cmbr2i  31566  cm2j  31590  fh3i  31593  fh4i  31594  pjaddii  31645  pjsslem  31649  pjssmii  31651  pjdifnormii  31653  lnopeq0lem1  31975  lnopunilem1  31980  lnophmlem2  31987  pjsdi2i  32127  pjclem1  32165  golem1  32241  dpmul100  32867  dpmul1000  32869  dpadd2  32880  dpadd  32881  dpadd3  32882  dpmul  32883  dpmul4  32884  ccatws1f1o  32922  elrgspnlem2  33200  matdim  33618  fldext2chn  33731  constrextdg2lem  33751  constrext2chnlem  33753  iconstr  33769  cos9thpiminplylem4  33788  cos9thpiminplylem5  33789  rmulccn  33931  raddcn  33932  xrmulc1cn  33933  xrge0iifhmeo  33939  qqh0  33987  qqh1  33988  elmbfmvol2  34270  mbfmcnt  34271  eulerpartlemgvv  34379  eulerpartlemgh  34381  fib2  34405  fib3  34406  fib4  34407  fib5  34408  fib6  34409  ballotlem2  34492  ballotlemfval0  34499  ballotth  34541  hgt750lem2  34655  problem2  35678  problem4  35680  quad3  35682  ditgeq123i  36222  cbvditgvw2  36262  poimirlem30  37669  iblabsnclem  37702  dalem10  39691  cdleme0e  40235  cdleme7c  40263  cdleme20c  40329  3exp7  42065  3lexlogpow5ineq1  42066  3lexlogpow5ineq5  42072  aks4d1p1  42088  5bc2eq10  42154  aks5lem3a  42201  sn-1ne2  42277  sqmid3api  42295  sqdeccom12  42301  sq3deccom12  42302  tan3rdpi  42364  sin2t3rdpi  42365  cos2t3rdpi  42366  rei4  42436  ipiiie0  42450  sn-0tie0  42463  mzpcompact2lem  42763  pellexlem5  42845  pellfundgt1  42895  jm2.27c  43019  areaquad  43228  resqrtvalex  43657  imsqrtvalex  43658  lhe4.4ex1a  44341  mccl  45617  dvnprodlem2  45964  itgsin0pilem1  45967  stoweidlem13  46030  wallispilem4  46085  wallispi2lem1  46088  wallispi2lem2  46089  dirkerper  46113  dirkertrigeqlem1  46115  fourierdlem30  46154  fourierdlem47  46170  fourierdlem103  46226  fourierdlem104  46227  fouriersw  46248  etransclem37  46288  sge0splitmpt  46428  sge0xaddlem2  46451  sge0xadd  46452  caragen0  46523  caragenuncllem  46529  fsumsplitsndif  47383  139prmALT  47606  127prm  47609  m11nprm  47611  3exp4mod41  47626  sbgoldbo  47797  2t6m3t4e0  48358  lincsum  48440  zlmodzxzequa  48507  zlmodzxzequap  48510  zlmodzxzldeplem3  48513  rrx2linest  48753  line2  48763  itsclc0yqsollem1  48773  itsclquadb  48787  itscnhlinecirc02plem2  48794  postcofval  49375  postcofcl  49376  precofval  49378  precofvalALT  49379  precofcl  49381  termcfuncval  49543