Theorem oveq12i 7358

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

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

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 2113  ax-9 2121  ax-ext 2703

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 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-iota 6437  df-fv 6489  df-ov 7349

This theorem is referenced by:  oveq123i  7360  caovdir  7580  caovdilem  7581  caovlem2  7582  cnfcom2  9592  canthwelem  10541  adderpqlem  10845  addassnq  10849  distrnq  10852  ltanq  10862  1lt2nq  10864  ltexnq  10866  halfnq  10867  mulcmpblnrlem  10961  mulcomsr  10980  distrsr  10982  m1p1sr  10983  m1m1sr  10984  mulgt0sr  10996  addcnsrec  11034  mulcnsrec  11035  axmulcom  11046  axmulass  11048  axdistr  11049  axi2m1  11050  addrid  11293  3t3e9  12287  8th4div3  12341  halfthird  12342  numma  12632  decmul10add  12657  4t3lem  12685  9t11e99  12718  5recm6rec  12731  fz0to3un2pr  13529  seqfeq4  13958  seqof  13966  sqdivi  14092  sq4e2t8  14106  i4  14111  binom2i  14119  nn0opthlem1  14175  facp1  14185  fac2  14186  fac3  14187  fac4  14188  faclbnd4lem1  14200  4bc2eq6  14236  ccat2s1len  14531  ccat2s1p2  14538  cats1len  14767  cats2cat  14769  ofs2  14878  cji  15066  01sqrexlem5  15153  fsumadd  15647  fsumsplitf  15649  fsumsplitsnun  15662  0.999...  15788  fprodmul  15867  fproddiv  15868  fprodsplitf  15895  bpoly3  15965  fsumcube  15967  efsep  16019  ef01bndlem  16093  cos2bnd  16097  rpnnen2lem3  16125  3dvds2dec  16244  flodddiv4  16326  sadeq  16383  gcdaddmlem  16435  bezout  16454  nn0expgcd  16475  nn0gcdsq  16663  pythagtriplem16  16742  4sqlem19  16875  dec5nprm  16978  dec2nprm  16979  mod2xnegi  16983  numexp2x  16990  decsplit  16994  karatsuba  16995  2exp5  16997  2exp11  17001  2exp16  17002  37prm  17032  43prm  17033  83prm  17034  139prm  17035  163prm  17036  317prm  17037  631prm  17038  1259lem1  17042  1259lem2  17043  1259lem3  17044  1259lem4  17045  1259lem5  17046  1259prm  17047  2503lem1  17048  2503lem2  17049  2503lem3  17050  2503prm  17051  4001lem1  17052  4001lem2  17053  4001lem3  17054  4001lem4  17055  4001prm  17056  funcoppc  17782  estrchom  18033  funcestrcsetclem5  18050  yonedalem3b  18185  ecqusaddd  19104  symgressbas  19294  gsum2dlem2  19883  gsumle  20057  opprrng  20263  isrhm  20396  rngqiprnglinlem2  21229  pzriprng1ALT  21433  evlsval  22021  mamudi  22318  mamudir  22319  oftpos  22367  mamutpos  22373  mdetrlin  22517  mdetrlin2  22522  mdetunilem5  22531  cpmadugsumfi  22792  cnmpt2res  23592  ussval  24174  icopnfhmeo  24868  iccpnfhmeo  24870  pcoass  24951  ovolunlem1a  25424  ioombl1lem3  25488  ioombl1lem4  25489  mbfimaopnlem  25583  itgfsum  25755  iblabslem  25756  itgsplit  25764  dveflem  25910  efhalfpi  26407  efipi  26409  sin2pi  26411  ef2pi  26413  sincosq3sgn  26436  sincosq4sgn  26437  sinq34lt0t  26445  sincos4thpi  26449  tan4thpi  26450  tan4thpiOLD  26451  sincos6thpi  26452  sincos3rdpi  26453  pigt3  26454  pige3ALT  26456  cxpcn3  26685  lawcos  26753  1cubrlem  26778  quart1lem  26792  quart1  26793  asin1  26831  atancj  26847  atanlogsublem  26852  log2cnv  26881  log2tlbnd  26882  log2ublem3  26885  log2ub  26886  birthday  26891  basellem8  27025  basellem9  27026  cht2  27109  cht3  27110  1sgm2ppw  27138  bclbnd  27218  bposlem8  27229  bposlem9  27230  lgsdi  27272  lgsquadlem1  27318  2lgsoddprmlem3c  27350  2lgsoddprmlem3d  27351  addsqnreup  27381  addsval2  27906  addsunif  27945  addsasslem1  27946  addsasslem2  27947  negsval  27967  negs0s  27968  negs1s  27969  negsid  27983  mulsval2  28050  muls01  28051  mulsproplem2  28056  mulsproplem3  28057  mulsproplem4  28058  mulsproplem5  28059  mulsproplem6  28060  mulsproplem7  28061  mulsproplem8  28062  mulsproplem12  28066  mulsproplem13  28067  mulsproplem14  28068  mulsunif  28089  addsdilem1  28090  addsdilem2  28091  mulsasslem1  28102  mulsasslem2  28103  mulsunif2  28109  precsexlem11  28155  onmulscl  28211  1p1e2s  28339  twocut  28346  0reno  28399  mirauto  28662  axsegconlem9  28903  ax5seglem7  28913  vtxdginducedm1  29522  clwlkclwwlkfo  29989  eupth2eucrct  30197  ex-exp  30430  ex-fac  30431  ex-bc  30432  ex-hash  30433  ip0i  30805  ip1ilem  30806  ip2i  30808  ipdirilem  30809  ipasslem10  30819  ip2dii  30824  pythi  30830  siilem1  30831  hvsubsub4i  31039  hvsubcan2i  31044  hisubcomi  31084  normlem0  31089  normlem1  31090  normlem2  31091  normlem3  31092  normlem6  31095  normlem8  31097  normlem9  31098  bcseqi  31100  norm-ii-i  31117  norm-iii-i  31119  normpythi  31122  norm3difi  31127  normpari  31134  normpar2i  31136  polid2i  31137  polidi  31138  bcsiALT  31159  lediri  31517  h1de2i  31533  cmcmlem  31571  cmbr2i  31576  cm2j  31600  fh3i  31603  fh4i  31604  pjaddii  31655  pjsslem  31659  pjssmii  31661  pjdifnormii  31663  lnopeq0lem1  31985  lnopunilem1  31990  lnophmlem2  31997  pjsdi2i  32137  pjclem1  32175  golem1  32251  dpmul100  32877  dpmul1000  32879  dpadd2  32890  dpadd  32891  dpadd3  32892  dpmul  32893  dpmul4  32894  ccatws1f1o  32932  elrgspnlem2  33210  matdim  33628  fldext2chn  33741  constrextdg2lem  33761  constrext2chnlem  33763  iconstr  33779  cos9thpiminplylem4  33798  cos9thpiminplylem5  33799  rmulccn  33941  raddcn  33942  xrmulc1cn  33943  xrge0iifhmeo  33949  qqh0  33997  qqh1  33998  elmbfmvol2  34280  mbfmcnt  34281  eulerpartlemgvv  34389  eulerpartlemgh  34391  fib2  34415  fib3  34416  fib4  34417  fib5  34418  fib6  34419  ballotlem2  34502  ballotlemfval0  34509  ballotth  34551  hgt750lem2  34665  problem2  35710  problem4  35712  quad3  35714  ditgeq123i  36253  cbvditgvw2  36293  poimirlem30  37689  iblabsnclem  37722  dalem10  39771  cdleme0e  40315  cdleme7c  40343  cdleme20c  40409  3exp7  42145  3lexlogpow5ineq1  42146  3lexlogpow5ineq5  42152  aks4d1p1  42168  5bc2eq10  42234  aks5lem3a  42281  sn-1ne2  42357  sqmid3api  42375  sqdeccom12  42381  sq3deccom12  42382  tan3rdpi  42444  sin2t3rdpi  42445  cos2t3rdpi  42446  rei4  42516  ipiiie0  42530  sn-0tie0  42543  mzpcompact2lem  42843  pellexlem5  42925  pellfundgt1  42975  jm2.27c  43099  areaquad  43308  resqrtvalex  43737  imsqrtvalex  43738  lhe4.4ex1a  44421  mccl  45697  dvnprodlem2  46044  itgsin0pilem1  46047  stoweidlem13  46110  wallispilem4  46165  wallispi2lem1  46168  wallispi2lem2  46169  dirkerper  46193  dirkertrigeqlem1  46195  fourierdlem30  46234  fourierdlem47  46250  fourierdlem103  46306  fourierdlem104  46307  fouriersw  46328  etransclem37  46368  sge0splitmpt  46508  sge0xaddlem2  46531  sge0xadd  46532  caragen0  46603  caragenuncllem  46609  nthrucw  46983  fsumsplitsndif  47472  139prmALT  47695  127prm  47698  m11nprm  47700  3exp4mod41  47715  sbgoldbo  47886  2t6m3t4e0  48447  lincsum  48529  zlmodzxzequa  48596  zlmodzxzequap  48599  zlmodzxzldeplem3  48602  rrx2linest  48842  line2  48852  itsclc0yqsollem1  48862  itsclquadb  48876  itscnhlinecirc02plem2  48883  postcofval  49464  postcofcl  49465  precofval  49467  precofvalALT  49468  precofcl  49470  termcfuncval  49632