Theorem oveq12i 7436

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

Syntax hints:   = wceq 1534  (class class class)co 7424

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rab 3420  df-v 3464  df-dif 3950  df-un 3952  df-ss 3964  df-nul 4326  df-if 4534  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-br 5154  df-iota 6506  df-fv 6562  df-ov 7427

This theorem is referenced by:  oveq123i  7438  caovdir  7660  caovdilem  7661  caovlem2  7662  cnfcom2  9745  canthwelem  10693  adderpqlem  10997  addassnq  11001  distrnq  11004  ltanq  11014  1lt2nq  11016  ltexnq  11018  halfnq  11019  mulcmpblnrlem  11113  mulcomsr  11132  distrsr  11134  m1p1sr  11135  m1m1sr  11136  mulgt0sr  11148  addcnsrec  11186  mulcnsrec  11187  axmulcom  11198  axmulass  11200  axdistr  11201  axi2m1  11202  addrid  11444  3t3e9  12431  8th4div3  12484  halfpm6th  12485  numma  12773  decmul10add  12798  4t3lem  12826  9t11e99  12859  halfthird  12872  5recm6rec  12873  fz0to3un2pr  13657  seqfeq4  14071  seqof  14079  sqdivi  14203  sq4e2t8  14217  i4  14222  binom2i  14230  nn0opthlem1  14285  facp1  14295  fac2  14296  fac3  14297  fac4  14298  faclbnd4lem1  14310  4bc2eq6  14346  ccat2s1len  14631  ccat2s1p2  14638  cats1len  14869  cats2cat  14871  ofs2  14976  cji  15164  01sqrexlem5  15251  fsumadd  15744  fsumsplitf  15746  fsumsplitsnun  15759  0.999...  15885  fprodmul  15962  fproddiv  15963  fprodsplitf  15990  bpoly3  16060  fsumcube  16062  efsep  16112  ef01bndlem  16186  cos2bnd  16190  rpnnen2lem3  16218  3dvds2dec  16335  flodddiv4  16415  sadeq  16472  gcdaddmlem  16524  bezout  16544  nn0expgcd  16565  nn0gcdsq  16754  pythagtriplem16  16832  4sqlem19  16965  dec5nprm  17068  dec2nprm  17069  mod2xnegi  17073  numexp2x  17081  decsplit  17085  karatsuba  17086  2exp5  17088  2exp11  17092  2exp16  17093  37prm  17123  43prm  17124  83prm  17125  139prm  17126  163prm  17127  317prm  17128  631prm  17129  1259lem1  17133  1259lem2  17134  1259lem3  17135  1259lem4  17136  1259lem5  17137  1259prm  17138  2503lem1  17139  2503lem2  17140  2503lem3  17141  2503prm  17142  4001lem1  17143  4001lem2  17144  4001lem3  17145  4001lem4  17146  4001prm  17147  funcoppc  17894  estrchom  18150  funcestrcsetclem5  18168  yonedalem3b  18304  ecqusaddd  19186  symgressbas  19379  gsum2dlem2  19969  opprrng  20327  isrhm  20460  rngqiprnglinlem2  21281  pzriprng1ALT  21486  evlsval  22101  mamudi  22394  mamudir  22395  oftpos  22445  mamutpos  22451  mdetrlin  22595  mdetrlin2  22600  mdetunilem5  22609  cpmadugsumfi  22870  cnmpt2res  23672  ussval  24255  icopnfhmeo  24959  iccpnfhmeo  24961  pcoass  25042  ovolunlem1a  25516  ioombl1lem3  25580  ioombl1lem4  25581  mbfimaopnlem  25675  itgfsum  25847  iblabslem  25848  itgsplit  25856  dveflem  26002  efhalfpi  26499  efipi  26501  sin2pi  26503  ef2pi  26505  sincosq3sgn  26528  sincosq4sgn  26529  sinq34lt0t  26537  sincos4thpi  26541  tan4thpi  26542  sincos6thpi  26543  sincos3rdpi  26544  pigt3  26545  pige3ALT  26547  cxpcn3  26776  lawcos  26844  1cubrlem  26869  quart1lem  26883  quart1  26884  asin1  26922  atancj  26938  atanlogsublem  26943  log2cnv  26972  log2tlbnd  26973  log2ublem3  26976  log2ub  26977  birthday  26982  basellem8  27116  basellem9  27117  cht2  27200  cht3  27201  1sgm2ppw  27229  bclbnd  27309  bposlem8  27320  bposlem9  27321  lgsdi  27363  lgsquadlem1  27409  2lgsoddprmlem3c  27441  2lgsoddprmlem3d  27442  addsqnreup  27472  addsval2  27977  addsunif  28016  addsasslem1  28017  addsasslem2  28018  negsval  28035  negs0s  28036  negsid  28050  mulsval2  28112  muls01  28113  mulsproplem2  28118  mulsproplem3  28119  mulsproplem4  28120  mulsproplem5  28121  mulsproplem6  28122  mulsproplem7  28123  mulsproplem8  28124  mulsproplem12  28128  mulsproplem13  28129  mulsproplem14  28130  mulsunif  28151  addsdilem1  28152  addsdilem2  28153  mulsasslem1  28164  mulsasslem2  28165  mulsunif2  28171  precsexlem11  28216  0reno  28348  mirauto  28611  axsegconlem9  28859  ax5seglem7  28869  vtxdginducedm1  29480  clwlkclwwlkfo  29942  eupth2eucrct  30150  ex-exp  30383  ex-fac  30384  ex-bc  30385  ex-hash  30386  ip0i  30758  ip1ilem  30759  ip2i  30761  ipdirilem  30762  ipasslem10  30772  ip2dii  30777  pythi  30783  siilem1  30784  hvsubsub4i  30992  hvsubcan2i  30997  hisubcomi  31037  normlem0  31042  normlem1  31043  normlem2  31044  normlem3  31045  normlem6  31048  normlem8  31050  normlem9  31051  bcseqi  31053  norm-ii-i  31070  norm-iii-i  31072  normpythi  31075  norm3difi  31080  normpari  31087  normpar2i  31089  polid2i  31090  polidi  31091  bcsiALT  31112  lediri  31470  h1de2i  31486  cmcmlem  31524  cmbr2i  31529  cm2j  31553  fh3i  31556  fh4i  31557  pjaddii  31608  pjsslem  31612  pjssmii  31614  pjdifnormii  31616  lnopeq0lem1  31938  lnopunilem1  31943  lnophmlem2  31950  pjsdi2i  32090  pjclem1  32128  golem1  32204  dpmul100  32758  dpmul1000  32760  dpadd2  32771  dpadd  32772  dpadd3  32773  dpmul  32774  dpmul4  32775  ccatws1f1o  32815  gsumle  32959  matdim  33510  rmulccn  33743  raddcn  33744  xrmulc1cn  33745  xrge0iifhmeo  33751  qqh0  33799  qqh1  33800  elmbfmvol2  34101  mbfmcnt  34102  eulerpartlemgvv  34210  eulerpartlemgh  34212  fib2  34236  fib3  34237  fib4  34238  fib5  34239  fib6  34240  ballotlem2  34322  ballotlemfval0  34329  ballotth  34371  hgt750lem2  34498  problem2  35494  problem4  35496  quad3  35498  poimirlem30  37351  iblabsnclem  37384  dalem10  39372  cdleme0e  39916  cdleme7c  39944  cdleme20c  40010  3exp7  41752  3lexlogpow5ineq1  41753  3lexlogpow5ineq5  41759  aks4d1p1  41775  5bc2eq10  41840  aks5lem3a  41887  sn-1ne2  42079  sqmid3api  42096  sqdeccom12  42102  sq3deccom12  42103  rei4  42203  ipiiie0  42217  sn-0tie0  42219  mzpcompact2lem  42408  pellexlem5  42490  pellfundgt1  42540  jm2.27c  42665  areaquad  42881  resqrtvalex  43312  imsqrtvalex  43313  lhe4.4ex1a  44003  mccl  45219  dvnprodlem2  45568  itgsin0pilem1  45571  stoweidlem13  45634  wallispilem4  45689  wallispi2lem1  45692  wallispi2lem2  45693  dirkerper  45717  dirkertrigeqlem1  45719  fourierdlem30  45758  fourierdlem47  45774  fourierdlem103  45830  fourierdlem104  45831  fouriersw  45852  etransclem37  45892  sge0splitmpt  46032  sge0xaddlem2  46055  sge0xadd  46056  caragen0  46127  caragenuncllem  46133  fsumsplitsndif  46945  139prmALT  47168  127prm  47171  m11nprm  47173  3exp4mod41  47188  sbgoldbo  47359  2t6m3t4e0  47727  lincsum  47812  zlmodzxzequa  47879  zlmodzxzequap  47882  zlmodzxzldeplem3  47885  rrx2linest  48130  line2  48140  itsclc0yqsollem1  48150  itsclquadb  48164  itscnhlinecirc02plem2  48171