Theorem oveq12i 7421

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

Syntax hints:   = wceq 1542  (class class class)co 7409

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412

This theorem is referenced by:  oveq123i  7423  caovdir  7641  caovdilem  7642  caovlem2  7643  cnfcom2  9697  canthwelem  10645  adderpqlem  10949  addassnq  10953  distrnq  10956  ltanq  10966  1lt2nq  10968  ltexnq  10970  halfnq  10971  mulcmpblnrlem  11065  mulcomsr  11084  distrsr  11086  m1p1sr  11087  m1m1sr  11088  mulgt0sr  11100  addcnsrec  11138  mulcnsrec  11139  axmulcom  11150  axmulass  11152  axdistr  11153  axi2m1  11154  addrid  11394  3t3e9  12379  8th4div3  12432  halfpm6th  12433  numma  12721  decmul10add  12746  4t3lem  12774  9t11e99  12807  halfthird  12820  5recm6rec  12821  fz0to3un2pr  13603  seqfeq4  14017  seqof  14025  sqdivi  14149  sq4e2t8  14163  i4  14168  binom2i  14176  nn0opthlem1  14228  facp1  14238  fac2  14239  fac3  14240  fac4  14241  faclbnd4lem1  14253  4bc2eq6  14289  ccat2s1len  14573  ccat2s1p2  14580  cats1len  14811  cats2cat  14813  ofs2  14918  cji  15106  01sqrexlem5  15193  fsumadd  15686  fsumsplitf  15688  fsumsplitsnun  15701  0.999...  15827  fprodmul  15904  fproddiv  15905  fprodsplitf  15932  bpoly3  16002  fsumcube  16004  efsep  16053  ef01bndlem  16127  cos2bnd  16131  rpnnen2lem3  16159  3dvds2dec  16276  flodddiv4  16356  sadeq  16413  gcdaddmlem  16465  bezout  16485  nn0gcdsq  16688  pythagtriplem16  16763  4sqlem19  16896  dec5nprm  16999  dec2nprm  17000  mod2xnegi  17004  numexp2x  17012  decsplit  17016  karatsuba  17017  2exp5  17019  2exp11  17023  2exp16  17024  37prm  17054  43prm  17055  83prm  17056  139prm  17057  163prm  17058  317prm  17059  631prm  17060  1259lem1  17064  1259lem2  17065  1259lem3  17066  1259lem4  17067  1259lem5  17068  1259prm  17069  2503lem1  17070  2503lem2  17071  2503lem3  17072  2503prm  17073  4001lem1  17074  4001lem2  17075  4001lem3  17076  4001lem4  17077  4001prm  17078  funcoppc  17825  estrchom  18078  funcestrcsetclem5  18096  yonedalem3b  18232  symgressbas  19249  gsum2dlem2  19839  opprring  20161  isrhm  20257  evlsval  21649  mamudi  21903  mamudir  21904  oftpos  21954  mamutpos  21960  mdetrlin  22104  mdetrlin2  22109  mdetunilem5  22118  cpmadugsumfi  22379  cnmpt2res  23181  ussval  23764  icopnfhmeo  24459  iccpnfhmeo  24461  pcoass  24540  ovolunlem1a  25013  ioombl1lem3  25077  ioombl1lem4  25078  mbfimaopnlem  25172  itgfsum  25344  iblabslem  25345  itgsplit  25353  dveflem  25496  efhalfpi  25981  efipi  25983  sin2pi  25985  ef2pi  25987  sincosq3sgn  26010  sincosq4sgn  26011  sinq34lt0t  26019  sincos4thpi  26023  tan4thpi  26024  sincos6thpi  26025  sincos3rdpi  26026  pigt3  26027  pige3ALT  26029  cxpcn3  26256  lawcos  26321  1cubrlem  26346  quart1lem  26360  quart1  26361  asin1  26399  atancj  26415  atanlogsublem  26420  log2cnv  26449  log2tlbnd  26450  log2ublem3  26453  log2ub  26454  birthday  26459  basellem8  26592  basellem9  26593  cht2  26676  cht3  26677  1sgm2ppw  26703  bclbnd  26783  bposlem8  26794  bposlem9  26795  lgsdi  26837  lgsquadlem1  26883  2lgsoddprmlem3c  26915  2lgsoddprmlem3d  26916  addsqnreup  26946  addsval2  27449  addsunif  27488  addsasslem1  27489  addsasslem2  27490  negsval  27503  negs0s  27504  negsid  27518  mulsval2  27570  muls01  27571  mulsproplem2  27576  mulsproplem3  27577  mulsproplem4  27578  mulsproplem5  27579  mulsproplem6  27580  mulsproplem7  27581  mulsproplem8  27582  mulsproplem12  27586  mulsproplem13  27587  mulsproplem14  27588  mulsunif  27608  addsdilem1  27609  addsdilem2  27610  mulsasslem1  27621  mulsasslem2  27622  precsexlem11  27666  mirauto  27966  axsegconlem9  28214  ax5seglem7  28224  vtxdginducedm1  28831  clwlkclwwlkfo  29293  eupth2eucrct  29501  ex-exp  29734  ex-fac  29735  ex-bc  29736  ex-hash  29737  ip0i  30109  ip1ilem  30110  ip2i  30112  ipdirilem  30113  ipasslem10  30123  ip2dii  30128  pythi  30134  siilem1  30135  hvsubsub4i  30343  hvsubcan2i  30348  hisubcomi  30388  normlem0  30393  normlem1  30394  normlem2  30395  normlem3  30396  normlem6  30399  normlem8  30401  normlem9  30402  bcseqi  30404  norm-ii-i  30421  norm-iii-i  30423  normpythi  30426  norm3difi  30431  normpari  30438  normpar2i  30440  polid2i  30441  polidi  30442  bcsiALT  30463  lediri  30821  h1de2i  30837  cmcmlem  30875  cmbr2i  30880  cm2j  30904  fh3i  30907  fh4i  30908  pjaddii  30959  pjsslem  30963  pjssmii  30965  pjdifnormii  30967  lnopeq0lem1  31289  lnopunilem1  31294  lnophmlem2  31301  pjsdi2i  31441  pjclem1  31479  golem1  31555  dpmul100  32094  dpmul1000  32096  dpadd2  32107  dpadd  32108  dpadd3  32109  dpmul  32110  dpmul4  32111  gsumle  32273  matdim  32731  rmulccn  32939  raddcn  32940  xrmulc1cn  32941  xrge0iifhmeo  32947  qqh0  32995  qqh1  32996  elmbfmvol2  33297  mbfmcnt  33298  eulerpartlemgvv  33406  eulerpartlemgh  33408  fib2  33432  fib3  33433  fib4  33434  fib5  33435  fib6  33436  ballotlem2  33518  ballotlemfval0  33525  ballotth  33567  hgt750lem2  33695  problem2  34682  problem4  34684  quad3  34686  gg-rmulccn  35210  poimirlem30  36566  iblabsnclem  36599  dalem10  38592  cdleme0e  39136  cdleme7c  39164  cdleme20c  39230  3exp7  40966  3lexlogpow5ineq1  40967  3lexlogpow5ineq5  40973  aks4d1p1  40989  5bc2eq10  41006  sn-1ne2  41227  sqmid3api  41243  sqdeccom12  41249  sq3deccom12  41250  nn0expgcd  41274  rei4  41344  ipiiie0  41358  sn-0tie0  41360  mzpcompact2lem  41537  pellexlem5  41619  pellfundgt1  41669  jm2.27c  41794  areaquad  42013  resqrtvalex  42444  imsqrtvalex  42445  lhe4.4ex1a  43136  mccl  44362  dvnprodlem2  44711  itgsin0pilem1  44714  stoweidlem13  44777  wallispilem4  44832  wallispi2lem1  44835  wallispi2lem2  44836  dirkerper  44860  dirkertrigeqlem1  44862  fourierdlem30  44901  fourierdlem47  44917  fourierdlem103  44973  fourierdlem104  44974  fouriersw  44995  etransclem37  45035  sge0splitmpt  45175  sge0xaddlem2  45198  sge0xadd  45199  caragen0  45270  caragenuncllem  45276  fsumsplitsndif  46089  139prmALT  46312  127prm  46315  m11nprm  46317  3exp4mod41  46332  sbgoldbo  46503  opprrng  46722  ecqusadd  46816  rngqiprnglinlem2  46825  pzriprng1ALT  46868  2t6m3t4e0  47072  lincsum  47158  zlmodzxzequa  47225  zlmodzxzequap  47228  zlmodzxzldeplem3  47231  rrx2linest  47476  line2  47486  itsclc0yqsollem1  47496  itsclquadb  47510  itscnhlinecirc02plem2  47517