Theorem oveq12i 7267

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258

This theorem is referenced by:  oveq123i  7269  caovdir  7484  caovdilem  7485  caovlem2  7486  cnfcom2  9390  canthwelem  10337  adderpqlem  10641  addassnq  10645  distrnq  10648  ltanq  10658  1lt2nq  10660  ltexnq  10662  halfnq  10663  mulcmpblnrlem  10757  mulcomsr  10776  distrsr  10778  m1p1sr  10779  m1m1sr  10780  mulgt0sr  10792  addcnsrec  10830  mulcnsrec  10831  axmulcom  10842  axmulass  10844  axdistr  10845  axi2m1  10846  addid1  11085  3t3e9  12070  8th4div3  12123  halfpm6th  12124  numma  12410  decmul10add  12435  4t3lem  12463  9t11e99  12496  halfthird  12509  5recm6rec  12510  fz0to3un2pr  13287  seqfeq4  13700  seqof  13708  sqdivi  13830  sq4e2t8  13844  i4  13849  binom2i  13856  nn0opthlem1  13910  facp1  13920  fac2  13921  fac3  13922  fac4  13923  faclbnd4lem1  13935  4bc2eq6  13971  ccat2s1len  14256  ccat2s1lenOLD  14257  ccat2s1p2  14265  ccat2s1p2OLD  14267  cats1len  14501  cats2cat  14503  ofs2  14610  cji  14798  sqrlem5  14886  fsumadd  15380  fsumsplitf  15382  fsumsplitsnun  15395  0.999...  15521  fprodmul  15598  fproddiv  15599  fprodsplitf  15626  bpoly3  15696  fsumcube  15698  efsep  15747  ef01bndlem  15821  cos2bnd  15825  rpnnen2lem3  15853  3dvds2dec  15970  flodddiv4  16050  sadeq  16107  gcdaddmlem  16159  bezout  16179  nn0gcdsq  16384  pythagtriplem16  16459  4sqlem19  16592  dec5nprm  16695  dec2nprm  16696  mod2xnegi  16700  numexp2x  16708  decsplit  16712  karatsuba  16713  2exp5  16715  2exp11  16719  2exp16  16720  37prm  16750  43prm  16751  83prm  16752  139prm  16753  163prm  16754  317prm  16755  631prm  16756  1259lem1  16760  1259lem2  16761  1259lem3  16762  1259lem4  16763  1259lem5  16764  1259prm  16765  2503lem1  16766  2503lem2  16767  2503lem3  16768  2503prm  16769  4001lem1  16770  4001lem2  16771  4001lem3  16772  4001lem4  16773  4001prm  16774  funcoppc  17506  estrchom  17759  funcestrcsetclem5  17777  yonedalem3b  17913  symgressbas  18904  gsum2dlem2  19487  opprring  19788  isrhm  19880  evlsval  21206  mamudi  21460  mamudir  21461  oftpos  21509  mamutpos  21515  mdetrlin  21659  mdetrlin2  21664  mdetunilem5  21673  cpmadugsumfi  21934  cnmpt2res  22736  ussval  23319  icopnfhmeo  24012  iccpnfhmeo  24014  pcoass  24093  ovolunlem1a  24565  ioombl1lem3  24629  ioombl1lem4  24630  mbfimaopnlem  24724  itgfsum  24896  iblabslem  24897  itgsplit  24905  dveflem  25048  efhalfpi  25533  efipi  25535  sin2pi  25537  ef2pi  25539  sincosq3sgn  25562  sincosq4sgn  25563  sinq34lt0t  25571  sincos4thpi  25575  tan4thpi  25576  sincos6thpi  25577  sincos3rdpi  25578  pigt3  25579  pige3ALT  25581  cxpcn3  25806  lawcos  25871  1cubrlem  25896  quart1lem  25910  quart1  25911  asin1  25949  atancj  25965  atanlogsublem  25970  log2cnv  25999  log2tlbnd  26000  log2ublem3  26003  log2ub  26004  birthday  26009  basellem8  26142  basellem9  26143  cht2  26226  cht3  26227  1sgm2ppw  26253  bclbnd  26333  bposlem8  26344  bposlem9  26345  lgsdi  26387  lgsquadlem1  26433  2lgsoddprmlem3c  26465  2lgsoddprmlem3d  26466  addsqnreup  26496  mirauto  26949  axsegconlem9  27196  ax5seglem7  27206  vtxdginducedm1  27813  clwlkclwwlkfo  28274  eupth2eucrct  28482  ex-exp  28715  ex-fac  28716  ex-bc  28717  ex-hash  28718  ip0i  29088  ip1ilem  29089  ip2i  29091  ipdirilem  29092  ipasslem10  29102  ip2dii  29107  pythi  29113  siilem1  29114  hvsubsub4i  29322  hvsubcan2i  29327  hisubcomi  29367  normlem0  29372  normlem1  29373  normlem2  29374  normlem3  29375  normlem6  29378  normlem8  29380  normlem9  29381  bcseqi  29383  norm-ii-i  29400  norm-iii-i  29402  normpythi  29405  norm3difi  29410  normpari  29417  normpar2i  29419  polid2i  29420  polidi  29421  bcsiALT  29442  lediri  29800  h1de2i  29816  cmcmlem  29854  cmbr2i  29859  cm2j  29883  fh3i  29886  fh4i  29887  pjaddii  29938  pjsslem  29942  pjssmii  29944  pjdifnormii  29946  lnopeq0lem1  30268  lnopunilem1  30273  lnophmlem2  30280  pjsdi2i  30420  pjclem1  30458  golem1  30534  dpmul100  31073  dpmul1000  31075  dpadd2  31086  dpadd  31087  dpadd3  31088  dpmul  31089  dpmul4  31090  gsumle  31252  matdim  31600  rmulccn  31780  raddcn  31781  xrmulc1cn  31782  xrge0iifhmeo  31788  qqh0  31834  qqh1  31835  elmbfmvol2  32134  mbfmcnt  32135  eulerpartlemgvv  32243  eulerpartlemgh  32245  fib2  32269  fib3  32270  fib4  32271  fib5  32272  fib6  32273  ballotlem2  32355  ballotlemfval0  32362  ballotth  32404  hgt750lem2  32532  problem2  33524  problem4  33526  quad3  33528  negsval  34050  negs0s  34051  poimirlem30  35734  iblabsnclem  35767  dalem10  37614  cdleme0e  38158  cdleme7c  38186  cdleme20c  38252  3exp7  39989  3lexlogpow5ineq1  39990  3lexlogpow5ineq5  39996  aks4d1p1  40012  5bc2eq10  40026  sn-1ne2  40216  sqmid3api  40232  sqdeccom12  40238  sq3deccom12  40239  nn0expgcd  40256  rei4  40326  ipiiie0  40340  sn-0tie0  40342  sn-0lt1  40353  mzpcompact2lem  40489  pellexlem5  40571  pellfundgt1  40621  jm2.27c  40745  areaquad  40963  resqrtvalex  41142  imsqrtvalex  41143  lhe4.4ex1a  41836  mccl  43029  dvnprodlem2  43378  itgsin0pilem1  43381  stoweidlem13  43444  wallispilem4  43499  wallispi2lem1  43502  wallispi2lem2  43503  dirkerper  43527  dirkertrigeqlem1  43529  fourierdlem30  43568  fourierdlem47  43584  fourierdlem103  43640  fourierdlem104  43641  fouriersw  43662  etransclem37  43702  sge0splitmpt  43839  sge0xaddlem2  43862  sge0xadd  43863  caragen0  43934  caragenuncllem  43940  fsumsplitsndif  44713  139prmALT  44936  127prm  44939  m11nprm  44941  3exp4mod41  44956  sbgoldbo  45127  2t6m3t4e0  45572  lincsum  45658  zlmodzxzequa  45725  zlmodzxzequap  45728  zlmodzxzldeplem3  45731  rrx2linest  45976  line2  45986  itsclc0yqsollem1  45996  itsclquadb  46010  itscnhlinecirc02plem2  46017