Theorem oveq12i 7452

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7440

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6509  df-fv 6563  df-ov 7443

This theorem is used by:  oveq123i  7454  caovdir  7676  caovdilem  7677  caovlem2  7678  cnfcom2  9727  canthwelem  10759  adderpqlem  11063  addassnq  11067  distrnq  11070  ltanq  11080  1lt2nq  11082  ltexnq  11084  halfnq  11085  mulcmpblnrlem  11179  mulcomsr  11198  distrsr  11200  m1p1sr  11201  m1m1sr  11202  mulgt0sr  11214  addcnsrec  11252  mulcnsrec  11253  axmulcom  11264  axmulass  11266  axdistr  11267  axi2m1  11268  addrid  11514  3t3e9  12534  8th4div3  12590  halfthird  12591  numma  12887  decmul10add  12912  4t3lem  12940  9t11e99OLD  12974  5recm6rec  12988  fz0to3un2pr  13787  seqfeq4  14218  seqof  14226  sqdivi  14352  sq4e2t8  14366  i4  14372  binom2i  14380  nn0opthlem1  14436  facp1  14446  fac2  14447  fac3  14448  fac4  14449  faclbnd4lem1  14461  4bc2eq6  14497  ccat2s1len  14796  ccat2s1p2  14803  cats1len  15036  cats2cat  15038  ofs2  15150  cji  15352  01sqrexlem5  15439  fsumadd  15932  fsumsplitf  15934  fsumsplitsnun  15947  0.999...  16076  fprodmul  16153  fproddiv  16154  fprodsplitf  16181  bpoly3  16250  fsumcube  16252  efsep  16304  ef01bndlem  16378  cos2bnd  16382  rpnnen2lem3  16410  3dvds2dec  16529  flodddiv4  16611  sadeq  16668  gcdaddmlem  16722  bezout  16742  nn0expgcd  16764  nn0gcdsq  16954  pythagtriplem16  17034  4sqlem19  17167  dec5nprm  17270  dec2nprm  17271  mod2xnegi  17275  numexp2x  17282  decsplit  17286  karatsuba  17287  2exp5  17289  2exp11  17293  2exp16  17294  37prm  17325  43prm  17326  83prm  17327  139prm  17328  163prm  17329  317prm  17330  631prm  17331  1259lem1  17335  1259lem2  17336  1259lem3  17337  1259lem4  17338  1259lem5  17339  1259prm  17340  2503lem1  17341  2503lem2  17342  2503lem3  17343  2503prm  17344  4001lem1  17345  4001lem2  17346  4001lem3  17347  4001lem4  17348  4001prm  17349  funcoppc  18076  estrchom  18327  funcestrcsetclem5  18344  yonedalem3b  18479  ecqusaddd  19433  symgressbas  19623  gsum2dlem2  20212  gsumle  20386  opprrng  20602  isrhm  20736  rngqiprnglinlem2  21615  pzriprng1ALT  21829  evlsval  22422  mamudi  22745  mamudir  22746  oftpos  22794  mamutpos  22800  mdetrlin  22944  mdetrlin2  22949  mdetunilem5  22958  cpmadugsumfi  23222  cnmpt2res  24023  ussval  24605  icopnfhmeo  25291  iccpnfhmeo  25293  pcoass  25372  ovolunlem1a  25844  ioombl1lem3  25908  ioombl1lem4  25909  mbfimaopnlem  26003  itgfsum  26174  iblabslem  26175  itgsplit  26183  dveflem  26326  efhalfpi  26827  efipi  26829  sin2pi  26831  ef2pi  26833  sincosq3sgn  26856  sincosq4sgn  26857  sinq34lt0t  26865  sincos4thpi  26869  tan4thpi  26870  sincos6thpi  26871  sincos3rdpi  26872  pigt3  26873  pige3ALT  26875  cxpcn3  27103  lawcos  27171  1cubrlem  27196  quart1lem  27210  quart1  27211  asin1  27249  atancj  27265  atanlogsublem  27270  log2cnv  27299  log2tlbnd  27300  log2ublem3  27303  log2ub  27304  birthday  27309  basellem8  27442  basellem9  27443  cht2  27526  cht3  27527  1sgm2ppw  27554  bclbnd  27634  bposlem8  27645  bposlem9  27646  lgsdi  27688  lgsquadlem1  27734  2lgsoddprmlem3c  27766  2lgsoddprmlem3d  27767  addsqnreup  27797  addsval2  28376  addsunif  28415  addsasslem1  28416  addsasslem2  28417  negsval  28438  neg0s  28439  neg1s  28440  negsid  28454  mulsval2  28524  muls01  28525  mulsproplem2  28530  mulsproplem3  28531  mulsproplem4  28532  mulsproplem5  28533  mulsproplem6  28534  mulsproplem7  28535  mulsproplem8  28536  mulsproplem12  28540  mulsproplem13  28541  mulsproplem14  28542  mulsunif  28563  addsdilem1  28564  addsdilem2  28565  mulsasslem1  28576  mulsasslem2  28577  mulsunif2  28583  precsexlem11  28630  onmulscl  28691  twocut  28836  mirauto  29183  axsegconlem9  29530  ax5seglem7  29540  vtxdginducedm1  30151  clwlkclwwlkfo  30627  eupth2eucrct  30845  ex-exp  31078  ex-fac  31079  ex-bc  31080  ex-hash  31081  ip0i  31454  ip1ilem  31455  ip2i  31457  ipdirilem  31458  ipasslem10  31468  ip2dii  31473  pythi  31479  siilem1  31480  hvsubsub4i  31688  hvsubcan2i  31693  hisubcomi  31733  normlem0  31738  normlem1  31739  normlem2  31740  normlem3  31741  normlem6  31744  normlem8  31746  normlem9  31747  bcseqi  31749  norm-ii-i  31766  norm-iii-i  31768  normpythi  31771  norm3difi  31776  normpari  31783  normpar2i  31785  polid2i  31786  polidi  31787  bcsiALT  31808  lediri  32166  h1de2i  32182  cmcmlem  32220  cmbr2i  32225  cm2j  32249  fh3i  32252  fh4i  32253  pjaddii  32304  pjsslem  32308  pjssmii  32310  pjdifnormii  32312  lnopeq0lem1  32634  lnopunilem1  32639  lnophmlem2  32646  pjsdi2i  32786  pjclem1  32824  golem1  32900  dpmul100  33530  dpmul1000  33532  dpadd2  33543  dpadd  33544  dpadd3  33545  dpmul  33546  dpmul4  33547  ccatws1f1o  33581  elrgspnlem2  33871  matdim  34314  fldext2chn  34427  constrextdg2lem  34447  constrext2chnlem  34449  iconstr  34465  cos9thpiminplylem4  34484  cos9thpiminplylem5  34485  rmulccn  34627  raddcn  34628  xrmulc1cn  34629  xrge0iifhmeo  34635  qqh0  34683  qqh1  34684  elmbfmvol2  34966  mbfmcnt  34967  eulerpartlemgvv  35075  eulerpartlemgh  35077  fib2  35101  fib3  35102  fib4  35103  fib5  35104  fib6  35105  ballotlem2  35188  ballotlemfval0  35195  ballotth  35237  hgt750lem2  35348  problem2  36597  problem4  36599  quad3  36601  ditgeq123i  37175  cbvditgvw2  37215  poimirlem30  38759  iblabsnclem  38792  dalem10  40921  cdleme0e  41465  cdleme7c  41493  cdleme20c  41559  3exp7  43294  3lexlogpow5ineq1  43295  3lexlogpow5ineq5  43301  aks4d1p1  43317  5bc2eq10  43383  aks5lem3a  43430  25or6to4  43447  sn-1ne2  43521  sqmid3api  43531  sqdeccom12  43537  sq3deccom12  43538  tan3rdpi  43594  sin2t3rdpi  43595  cos2t3rdpi  43596  rei4  43666  ipiiie0  43680  sn-0tie0  43706  mzpcompact2lem  43953  pellexlem5  44031  pellfundgt1  44081  jm2.27c  44205  areaquad  44408  resqrtvalex  44835  imsqrtvalex  44836  lhe4.4ex1a  45503  mccl  46813  dvnprodlem2  47160  itgsin0pilem1  47163  stoweidlem13  47226  wallispilem4  47281  wallispi2lem1  47284  wallispi2lem2  47285  dirkerper  47309  dirkertrigeqlem1  47311  fourierdlem30  47350  fourierdlem47  47366  fourierdlem103  47422  fourierdlem104  47423  fouriersw  47444  etransclem37  47484  sge0splitmpt  47624  sge0xaddlem2  47647  sge0xadd  47648  caragen0  47719  caragenuncllem  47725  goldpolyfactor  48130  goldrasin  48132  goldratmolem2  48136  goldratmolem3  48137  goldratval  48139  fsumsplitsndif  48654  139prmALT  48884  127prm  48887  m11nprm  48889  3exp4mod41  48904  ppivalnn4  48915  sbgoldbo  49088  2t6m3t4e0  49663  lincsum  49744  zlmodzxzequa  49811  zlmodzxzequap  49814  zlmodzxzldeplem3  49817  rrx2linest  50057  line2  50067  itsclc0yqsollem1  50077  itsclquadb  50091  itscnhlinecirc02plem2  50098  postcofval  50699  postcofcl  50700  precofval  50705  precofvalALT  50706  precofcl  50708  termcfuncval  50870  par2diag  50983