Theorem oveq12i 7381

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

Syntax hints:   = wceq 1540  (class class class)co 7369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372

This theorem is referenced by:  oveq123i  7383  caovdir  7603  caovdilem  7604  caovlem2  7605  cnfcom2  9631  canthwelem  10579  adderpqlem  10883  addassnq  10887  distrnq  10890  ltanq  10900  1lt2nq  10902  ltexnq  10904  halfnq  10905  mulcmpblnrlem  10999  mulcomsr  11018  distrsr  11020  m1p1sr  11021  m1m1sr  11022  mulgt0sr  11034  addcnsrec  11072  mulcnsrec  11073  axmulcom  11084  axmulass  11086  axdistr  11087  axi2m1  11088  addrid  11330  3t3e9  12324  8th4div3  12378  halfthird  12379  numma  12669  decmul10add  12694  4t3lem  12722  9t11e99  12755  5recm6rec  12768  fz0to3un2pr  13566  seqfeq4  13992  seqof  14000  sqdivi  14126  sq4e2t8  14140  i4  14145  binom2i  14153  nn0opthlem1  14209  facp1  14219  fac2  14220  fac3  14221  fac4  14222  faclbnd4lem1  14234  4bc2eq6  14270  ccat2s1len  14564  ccat2s1p2  14571  cats1len  14802  cats2cat  14804  ofs2  14913  cji  15101  01sqrexlem5  15188  fsumadd  15682  fsumsplitf  15684  fsumsplitsnun  15697  0.999...  15823  fprodmul  15902  fproddiv  15903  fprodsplitf  15930  bpoly3  16000  fsumcube  16002  efsep  16054  ef01bndlem  16128  cos2bnd  16132  rpnnen2lem3  16160  3dvds2dec  16279  flodddiv4  16361  sadeq  16418  gcdaddmlem  16470  bezout  16489  nn0expgcd  16510  nn0gcdsq  16698  pythagtriplem16  16777  4sqlem19  16910  dec5nprm  17013  dec2nprm  17014  mod2xnegi  17018  numexp2x  17025  decsplit  17029  karatsuba  17030  2exp5  17032  2exp11  17036  2exp16  17037  37prm  17067  43prm  17068  83prm  17069  139prm  17070  163prm  17071  317prm  17072  631prm  17073  1259lem1  17077  1259lem2  17078  1259lem3  17079  1259lem4  17080  1259lem5  17081  1259prm  17082  2503lem1  17083  2503lem2  17084  2503lem3  17085  2503prm  17086  4001lem1  17087  4001lem2  17088  4001lem3  17089  4001lem4  17090  4001prm  17091  funcoppc  17817  estrchom  18068  funcestrcsetclem5  18085  yonedalem3b  18220  ecqusaddd  19106  symgressbas  19296  gsum2dlem2  19885  gsumle  20059  opprrng  20265  isrhm  20398  rngqiprnglinlem2  21234  pzriprng1ALT  21438  evlsval  22026  mamudi  22323  mamudir  22324  oftpos  22372  mamutpos  22378  mdetrlin  22522  mdetrlin2  22527  mdetunilem5  22536  cpmadugsumfi  22797  cnmpt2res  23597  ussval  24180  icopnfhmeo  24874  iccpnfhmeo  24876  pcoass  24957  ovolunlem1a  25430  ioombl1lem3  25494  ioombl1lem4  25495  mbfimaopnlem  25589  itgfsum  25761  iblabslem  25762  itgsplit  25770  dveflem  25916  efhalfpi  26413  efipi  26415  sin2pi  26417  ef2pi  26419  sincosq3sgn  26442  sincosq4sgn  26443  sinq34lt0t  26451  sincos4thpi  26455  tan4thpi  26456  tan4thpiOLD  26457  sincos6thpi  26458  sincos3rdpi  26459  pigt3  26460  pige3ALT  26462  cxpcn3  26691  lawcos  26759  1cubrlem  26784  quart1lem  26798  quart1  26799  asin1  26837  atancj  26853  atanlogsublem  26858  log2cnv  26887  log2tlbnd  26888  log2ublem3  26891  log2ub  26892  birthday  26897  basellem8  27031  basellem9  27032  cht2  27115  cht3  27116  1sgm2ppw  27144  bclbnd  27224  bposlem8  27235  bposlem9  27236  lgsdi  27278  lgsquadlem1  27324  2lgsoddprmlem3c  27356  2lgsoddprmlem3d  27357  addsqnreup  27387  addsval2  27910  addsunif  27949  addsasslem1  27950  addsasslem2  27951  negsval  27971  negs0s  27972  negs1s  27973  negsid  27987  mulsval2  28054  muls01  28055  mulsproplem2  28060  mulsproplem3  28061  mulsproplem4  28062  mulsproplem5  28063  mulsproplem6  28064  mulsproplem7  28065  mulsproplem8  28066  mulsproplem12  28070  mulsproplem13  28071  mulsproplem14  28072  mulsunif  28093  addsdilem1  28094  addsdilem2  28095  mulsasslem1  28106  mulsasslem2  28107  mulsunif2  28113  precsexlem11  28159  onmulscl  28215  1p1e2s  28343  twocut  28350  0reno  28401  mirauto  28664  axsegconlem9  28905  ax5seglem7  28915  vtxdginducedm1  29524  clwlkclwwlkfo  29988  eupth2eucrct  30196  ex-exp  30429  ex-fac  30430  ex-bc  30431  ex-hash  30432  ip0i  30804  ip1ilem  30805  ip2i  30807  ipdirilem  30808  ipasslem10  30818  ip2dii  30823  pythi  30829  siilem1  30830  hvsubsub4i  31038  hvsubcan2i  31043  hisubcomi  31083  normlem0  31088  normlem1  31089  normlem2  31090  normlem3  31091  normlem6  31094  normlem8  31096  normlem9  31097  bcseqi  31099  norm-ii-i  31116  norm-iii-i  31118  normpythi  31121  norm3difi  31126  normpari  31133  normpar2i  31135  polid2i  31136  polidi  31137  bcsiALT  31158  lediri  31516  h1de2i  31532  cmcmlem  31570  cmbr2i  31575  cm2j  31599  fh3i  31602  fh4i  31603  pjaddii  31654  pjsslem  31658  pjssmii  31660  pjdifnormii  31662  lnopeq0lem1  31984  lnopunilem1  31989  lnophmlem2  31996  pjsdi2i  32136  pjclem1  32174  golem1  32250  dpmul100  32867  dpmul1000  32869  dpadd2  32880  dpadd  32881  dpadd3  32882  dpmul  32883  dpmul4  32884  ccatws1f1o  32923  elrgspnlem2  33210  matdim  33604  fldext2chn  33711  constrextdg2lem  33731  constrext2chnlem  33733  iconstr  33749  cos9thpiminplylem4  33768  cos9thpiminplylem5  33769  rmulccn  33911  raddcn  33912  xrmulc1cn  33913  xrge0iifhmeo  33919  qqh0  33967  qqh1  33968  elmbfmvol2  34251  mbfmcnt  34252  eulerpartlemgvv  34360  eulerpartlemgh  34362  fib2  34386  fib3  34387  fib4  34388  fib5  34389  fib6  34390  ballotlem2  34473  ballotlemfval0  34480  ballotth  34522  hgt750lem2  34636  problem2  35646  problem4  35648  quad3  35650  ditgeq123i  36190  cbvditgvw2  36230  poimirlem30  37637  iblabsnclem  37670  dalem10  39660  cdleme0e  40204  cdleme7c  40232  cdleme20c  40298  3exp7  42034  3lexlogpow5ineq1  42035  3lexlogpow5ineq5  42041  aks4d1p1  42057  5bc2eq10  42123  aks5lem3a  42170  sn-1ne2  42246  sqmid3api  42264  sqdeccom12  42270  sq3deccom12  42271  tan3rdpi  42333  sin2t3rdpi  42334  cos2t3rdpi  42335  rei4  42405  ipiiie0  42419  sn-0tie0  42432  mzpcompact2lem  42732  pellexlem5  42814  pellfundgt1  42864  jm2.27c  42989  areaquad  43198  resqrtvalex  43627  imsqrtvalex  43628  lhe4.4ex1a  44311  mccl  45589  dvnprodlem2  45938  itgsin0pilem1  45941  stoweidlem13  46004  wallispilem4  46059  wallispi2lem1  46062  wallispi2lem2  46063  dirkerper  46087  dirkertrigeqlem1  46089  fourierdlem30  46128  fourierdlem47  46144  fourierdlem103  46200  fourierdlem104  46201  fouriersw  46222  etransclem37  46262  sge0splitmpt  46402  sge0xaddlem2  46425  sge0xadd  46426  caragen0  46497  caragenuncllem  46503  fsumsplitsndif  47367  139prmALT  47590  127prm  47593  m11nprm  47595  3exp4mod41  47610  sbgoldbo  47781  2t6m3t4e0  48329  lincsum  48411  zlmodzxzequa  48478  zlmodzxzequap  48481  zlmodzxzldeplem3  48484  rrx2linest  48724  line2  48734  itsclc0yqsollem1  48744  itsclquadb  48758  itscnhlinecirc02plem2  48765  postcofval  49346  postcofcl  49347  precofval  49349  precofvalALT  49350  precofcl  49352  termcfuncval  49514