Theorem oveq12i 7432

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

This proof depends on syntax axioms:   = wceq 1569  (class class class)co 7420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423

This theorem is used by:  oveq123i  7434  caovdir  7655  caovdilem  7656  caovlem2  7657  cnfcom2  9703  canthwelem  10735  adderpqlem  11039  addassnq  11043  distrnq  11046  ltanq  11056  1lt2nq  11058  ltexnq  11060  halfnq  11061  mulcmpblnrlem  11155  mulcomsr  11174  distrsr  11176  m1p1sr  11177  m1m1sr  11178  mulgt0sr  11190  addcnsrec  11228  mulcnsrec  11229  axmulcom  11240  axmulass  11242  axdistr  11243  axi2m1  11244  addrid  11490  3t3e9  12510  8th4div3  12566  halfthird  12567  numma  12863  decmul10add  12888  4t3lem  12916  9t11e99OLD  12950  5recm6rec  12964  fz0to3un2pr  13763  seqfeq4  14194  seqof  14202  sqdivi  14328  sq4e2t8  14342  i4  14348  binom2i  14356  nn0opthlem1  14412  facp1  14422  fac2  14423  fac3  14424  fac4  14425  faclbnd4lem1  14437  4bc2eq6  14473  ccat2s1len  14771  ccat2s1p2  14778  cats1len  15011  cats2cat  15013  ofs2  15124  cji  15326  01sqrexlem5  15413  fsumadd  15906  fsumsplitf  15908  fsumsplitsnun  15921  0.999...  16050  fprodmul  16127  fproddiv  16128  fprodsplitf  16155  bpoly3  16224  fsumcube  16226  efsep  16278  ef01bndlem  16352  cos2bnd  16356  rpnnen2lem3  16384  3dvds2dec  16503  flodddiv4  16585  sadeq  16642  gcdaddmlem  16696  bezout  16716  nn0expgcd  16738  nn0gcdsq  16928  pythagtriplem16  17008  4sqlem19  17141  dec5nprm  17244  dec2nprm  17245  mod2xnegi  17249  numexp2x  17256  decsplit  17260  karatsuba  17261  2exp5  17263  2exp11  17267  2exp16  17268  37prm  17299  43prm  17300  83prm  17301  139prm  17302  163prm  17303  317prm  17304  631prm  17305  1259lem1  17309  1259lem2  17310  1259lem3  17311  1259lem4  17312  1259lem5  17313  1259prm  17314  2503lem1  17315  2503lem2  17316  2503lem3  17317  2503prm  17318  4001lem1  17319  4001lem2  17320  4001lem3  17321  4001lem4  17322  4001prm  17323  funcoppc  18050  estrchom  18301  funcestrcsetclem5  18318  yonedalem3b  18453  ecqusaddd  19407  symgressbas  19596  gsum2dlem2  20185  gsumle  20359  opprrng  20575  isrhm  20709  rngqiprnglinlem2  21588  pzriprng1ALT  21802  evlsval  22395  mamudi  22718  mamudir  22719  oftpos  22767  mamutpos  22773  mdetrlin  22917  mdetrlin2  22922  mdetunilem5  22931  cpmadugsumfi  23195  cnmpt2res  23996  ussval  24578  icopnfhmeo  25264  iccpnfhmeo  25266  pcoass  25345  ovolunlem1a  25817  ioombl1lem3  25881  ioombl1lem4  25882  mbfimaopnlem  25976  itgfsum  26147  iblabslem  26148  itgsplit  26156  dveflem  26299  efhalfpi  26800  efipi  26802  sin2pi  26804  ef2pi  26806  sincosq3sgn  26829  sincosq4sgn  26830  sinq34lt0t  26838  sincos4thpi  26842  tan4thpi  26843  sincos6thpi  26844  sincos3rdpi  26845  pigt3  26846  pige3ALT  26848  cxpcn3  27076  lawcos  27144  1cubrlem  27169  quart1lem  27183  quart1  27184  asin1  27222  atancj  27238  atanlogsublem  27243  log2cnv  27272  log2tlbnd  27273  log2ublem3  27276  log2ub  27277  birthday  27282  basellem8  27415  basellem9  27416  cht2  27499  cht3  27500  1sgm2ppw  27527  bclbnd  27607  bposlem8  27618  bposlem9  27619  lgsdi  27661  lgsquadlem1  27707  2lgsoddprmlem3c  27739  2lgsoddprmlem3d  27740  addsqnreup  27770  addsval2  28349  addsunif  28388  addsasslem1  28389  addsasslem2  28390  negsval  28411  neg0s  28412  neg1s  28413  negsid  28427  mulsval2  28497  muls01  28498  mulsproplem2  28503  mulsproplem3  28504  mulsproplem4  28505  mulsproplem5  28506  mulsproplem6  28507  mulsproplem7  28508  mulsproplem8  28509  mulsproplem12  28513  mulsproplem13  28514  mulsproplem14  28515  mulsunif  28536  addsdilem1  28537  addsdilem2  28538  mulsasslem1  28549  mulsasslem2  28550  mulsunif2  28556  precsexlem11  28603  onmulscl  28664  twocut  28809  mirauto  29156  axsegconlem9  29503  ax5seglem7  29513  vtxdginducedm1  30124  clwlkclwwlkfo  30600  eupth2eucrct  30818  ex-exp  31051  ex-fac  31052  ex-bc  31053  ex-hash  31054  ip0i  31427  ip1ilem  31428  ip2i  31430  ipdirilem  31431  ipasslem10  31441  ip2dii  31446  pythi  31452  siilem1  31453  hvsubsub4i  31661  hvsubcan2i  31666  hisubcomi  31706  normlem0  31711  normlem1  31712  normlem2  31713  normlem3  31714  normlem6  31717  normlem8  31719  normlem9  31720  bcseqi  31722  norm-ii-i  31739  norm-iii-i  31741  normpythi  31744  norm3difi  31749  normpari  31756  normpar2i  31758  polid2i  31759  polidi  31760  bcsiALT  31781  lediri  32139  h1de2i  32155  cmcmlem  32193  cmbr2i  32198  cm2j  32222  fh3i  32225  fh4i  32226  pjaddii  32277  pjsslem  32281  pjssmii  32283  pjdifnormii  32285  lnopeq0lem1  32607  lnopunilem1  32612  lnophmlem2  32619  pjsdi2i  32759  pjclem1  32797  golem1  32873  dpmul100  33463  dpmul1000  33465  dpadd2  33476  dpadd  33477  dpadd3  33478  dpmul  33479  dpmul4  33480  ccatws1f1o  33514  elrgspnlem2  33804  matdim  34247  fldext2chn  34360  constrextdg2lem  34380  constrext2chnlem  34382  iconstr  34398  cos9thpiminplylem4  34417  cos9thpiminplylem5  34418  rmulccn  34560  raddcn  34561  xrmulc1cn  34562  xrge0iifhmeo  34568  qqh0  34616  qqh1  34617  elmbfmvol2  34899  mbfmcnt  34900  eulerpartlemgvv  35008  eulerpartlemgh  35010  fib2  35034  fib3  35035  fib4  35036  fib5  35037  fib6  35038  ballotlem2  35121  ballotlemfval0  35128  ballotth  35170  hgt750lem2  35281  problem2  36431  problem4  36433  quad3  36435  ditgeq123i  36998  cbvditgvw2  37038  poimirlem30  38569  iblabsnclem  38602  dalem10  40731  cdleme0e  41275  cdleme7c  41303  cdleme20c  41369  3exp7  43104  3lexlogpow5ineq1  43105  3lexlogpow5ineq5  43111  aks4d1p1  43127  5bc2eq10  43193  aks5lem3a  43240  25or6to4  43257  sn-1ne2  43331  sqmid3api  43341  sqdeccom12  43347  sq3deccom12  43348  tan3rdpi  43404  sin2t3rdpi  43405  cos2t3rdpi  43406  rei4  43476  ipiiie0  43490  sn-0tie0  43516  mzpcompact2lem  43762  pellexlem5  43840  pellfundgt1  43890  jm2.27c  44014  areaquad  44218  resqrtvalex  44645  imsqrtvalex  44646  lhe4.4ex1a  45313  mccl  46610  dvnprodlem2  46957  itgsin0pilem1  46960  stoweidlem13  47023  wallispilem4  47078  wallispi2lem1  47081  wallispi2lem2  47082  dirkerper  47106  dirkertrigeqlem1  47108  fourierdlem30  47147  fourierdlem47  47163  fourierdlem103  47219  fourierdlem104  47220  fouriersw  47241  etransclem37  47281  sge0splitmpt  47421  sge0xaddlem2  47444  sge0xadd  47445  caragen0  47516  caragenuncllem  47522  goldpolyfactor  47927  goldrasin  47929  goldratmolem2  47933  goldratmolem3  47934  goldratval  47936  fsumsplitsndif  48451  139prmALT  48681  127prm  48684  m11nprm  48686  3exp4mod41  48701  ppivalnn4  48712  sbgoldbo  48885  2t6m3t4e0  49460  lincsum  49541  zlmodzxzequa  49608  zlmodzxzequap  49611  zlmodzxzldeplem3  49614  rrx2linest  49854  line2  49864  itsclc0yqsollem1  49874  itsclquadb  49888  itscnhlinecirc02plem2  49895  postcofval  50472  postcofcl  50473  precofval  50475  precofvalALT  50476  precofcl  50478  termcfuncval  50640