Theorem oveq12i 7296

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

Syntax hints:   = wceq 1539  (class class class)co 7284

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 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-iota 6395  df-fv 6445  df-ov 7287

This theorem is referenced by:  oveq123i  7298  caovdir  7515  caovdilem  7516  caovlem2  7517  cnfcom2  9469  canthwelem  10415  adderpqlem  10719  addassnq  10723  distrnq  10726  ltanq  10736  1lt2nq  10738  ltexnq  10740  halfnq  10741  mulcmpblnrlem  10835  mulcomsr  10854  distrsr  10856  m1p1sr  10857  m1m1sr  10858  mulgt0sr  10870  addcnsrec  10908  mulcnsrec  10909  axmulcom  10920  axmulass  10922  axdistr  10923  axi2m1  10924  addid1  11164  3t3e9  12149  8th4div3  12202  halfpm6th  12203  numma  12490  decmul10add  12515  4t3lem  12543  9t11e99  12576  halfthird  12589  5recm6rec  12590  fz0to3un2pr  13367  seqfeq4  13781  seqof  13789  sqdivi  13911  sq4e2t8  13925  i4  13930  binom2i  13937  nn0opthlem1  13991  facp1  14001  fac2  14002  fac3  14003  fac4  14004  faclbnd4lem1  14016  4bc2eq6  14052  ccat2s1len  14337  ccat2s1lenOLD  14338  ccat2s1p2  14346  ccat2s1p2OLD  14348  cats1len  14582  cats2cat  14584  ofs2  14691  cji  14879  sqrlem5  14967  fsumadd  15461  fsumsplitf  15463  fsumsplitsnun  15476  0.999...  15602  fprodmul  15679  fproddiv  15680  fprodsplitf  15707  bpoly3  15777  fsumcube  15779  efsep  15828  ef01bndlem  15902  cos2bnd  15906  rpnnen2lem3  15934  3dvds2dec  16051  flodddiv4  16131  sadeq  16188  gcdaddmlem  16240  bezout  16260  nn0gcdsq  16465  pythagtriplem16  16540  4sqlem19  16673  dec5nprm  16776  dec2nprm  16777  mod2xnegi  16781  numexp2x  16789  decsplit  16793  karatsuba  16794  2exp5  16796  2exp11  16800  2exp16  16801  37prm  16831  43prm  16832  83prm  16833  139prm  16834  163prm  16835  317prm  16836  631prm  16837  1259lem1  16841  1259lem2  16842  1259lem3  16843  1259lem4  16844  1259lem5  16845  1259prm  16846  2503lem1  16847  2503lem2  16848  2503lem3  16849  2503prm  16850  4001lem1  16851  4001lem2  16852  4001lem3  16853  4001lem4  16854  4001prm  16855  funcoppc  17599  estrchom  17852  funcestrcsetclem5  17870  yonedalem3b  18006  symgressbas  18998  gsum2dlem2  19581  opprring  19882  isrhm  19974  evlsval  21305  mamudi  21559  mamudir  21560  oftpos  21610  mamutpos  21616  mdetrlin  21760  mdetrlin2  21765  mdetunilem5  21774  cpmadugsumfi  22035  cnmpt2res  22837  ussval  23420  icopnfhmeo  24115  iccpnfhmeo  24117  pcoass  24196  ovolunlem1a  24669  ioombl1lem3  24733  ioombl1lem4  24734  mbfimaopnlem  24828  itgfsum  25000  iblabslem  25001  itgsplit  25009  dveflem  25152  efhalfpi  25637  efipi  25639  sin2pi  25641  ef2pi  25643  sincosq3sgn  25666  sincosq4sgn  25667  sinq34lt0t  25675  sincos4thpi  25679  tan4thpi  25680  sincos6thpi  25681  sincos3rdpi  25682  pigt3  25683  pige3ALT  25685  cxpcn3  25910  lawcos  25975  1cubrlem  26000  quart1lem  26014  quart1  26015  asin1  26053  atancj  26069  atanlogsublem  26074  log2cnv  26103  log2tlbnd  26104  log2ublem3  26107  log2ub  26108  birthday  26113  basellem8  26246  basellem9  26247  cht2  26330  cht3  26331  1sgm2ppw  26357  bclbnd  26437  bposlem8  26448  bposlem9  26449  lgsdi  26491  lgsquadlem1  26537  2lgsoddprmlem3c  26569  2lgsoddprmlem3d  26570  addsqnreup  26600  mirauto  27054  axsegconlem9  27302  ax5seglem7  27312  vtxdginducedm1  27919  clwlkclwwlkfo  28382  eupth2eucrct  28590  ex-exp  28823  ex-fac  28824  ex-bc  28825  ex-hash  28826  ip0i  29196  ip1ilem  29197  ip2i  29199  ipdirilem  29200  ipasslem10  29210  ip2dii  29215  pythi  29221  siilem1  29222  hvsubsub4i  29430  hvsubcan2i  29435  hisubcomi  29475  normlem0  29480  normlem1  29481  normlem2  29482  normlem3  29483  normlem6  29486  normlem8  29488  normlem9  29489  bcseqi  29491  norm-ii-i  29508  norm-iii-i  29510  normpythi  29513  norm3difi  29518  normpari  29525  normpar2i  29527  polid2i  29528  polidi  29529  bcsiALT  29550  lediri  29908  h1de2i  29924  cmcmlem  29962  cmbr2i  29967  cm2j  29991  fh3i  29994  fh4i  29995  pjaddii  30046  pjsslem  30050  pjssmii  30052  pjdifnormii  30054  lnopeq0lem1  30376  lnopunilem1  30381  lnophmlem2  30388  pjsdi2i  30528  pjclem1  30566  golem1  30642  dpmul100  31180  dpmul1000  31182  dpadd2  31193  dpadd  31194  dpadd3  31195  dpmul  31196  dpmul4  31197  gsumle  31359  matdim  31707  rmulccn  31887  raddcn  31888  xrmulc1cn  31889  xrge0iifhmeo  31895  qqh0  31943  qqh1  31944  elmbfmvol2  32243  mbfmcnt  32244  eulerpartlemgvv  32352  eulerpartlemgh  32354  fib2  32378  fib3  32379  fib4  32380  fib5  32381  fib6  32382  ballotlem2  32464  ballotlemfval0  32471  ballotth  32513  hgt750lem2  32641  problem2  33633  problem4  33635  quad3  33637  negsval  34132  negs0s  34133  poimirlem30  35816  iblabsnclem  35849  dalem10  37694  cdleme0e  38238  cdleme7c  38266  cdleme20c  38332  3exp7  40068  3lexlogpow5ineq1  40069  3lexlogpow5ineq5  40075  aks4d1p1  40091  5bc2eq10  40105  sn-1ne2  40302  sqmid3api  40318  sqdeccom12  40324  sq3deccom12  40325  nn0expgcd  40342  rei4  40412  ipiiie0  40426  sn-0tie0  40428  sn-0lt1  40439  mzpcompact2lem  40580  pellexlem5  40662  pellfundgt1  40712  jm2.27c  40836  areaquad  41054  resqrtvalex  41260  imsqrtvalex  41261  lhe4.4ex1a  41954  mccl  43146  dvnprodlem2  43495  itgsin0pilem1  43498  stoweidlem13  43561  wallispilem4  43616  wallispi2lem1  43619  wallispi2lem2  43620  dirkerper  43644  dirkertrigeqlem1  43646  fourierdlem30  43685  fourierdlem47  43701  fourierdlem103  43757  fourierdlem104  43758  fouriersw  43779  etransclem37  43819  sge0splitmpt  43956  sge0xaddlem2  43979  sge0xadd  43980  caragen0  44051  caragenuncllem  44057  fsumsplitsndif  44836  139prmALT  45059  127prm  45062  m11nprm  45064  3exp4mod41  45079  sbgoldbo  45250  2t6m3t4e0  45695  lincsum  45781  zlmodzxzequa  45848  zlmodzxzequap  45851  zlmodzxzldeplem3  45854  rrx2linest  46099  line2  46109  itsclc0yqsollem1  46119  itsclquadb  46133  itscnhlinecirc02plem2  46140