Theorem oveq12i 7170

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

Syntax hints:   = wceq 1537  (class class class)co 7158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-iota 6316  df-fv 6365  df-ov 7161

This theorem is referenced by:  oveq123i  7172  caovdir  7384  caovdilem  7385  caovlem2  7386  cnfcom2  9167  canthwelem  10074  adderpqlem  10378  addassnq  10382  distrnq  10385  ltanq  10395  1lt2nq  10397  ltexnq  10399  halfnq  10400  mulcmpblnrlem  10494  mulcomsr  10513  distrsr  10515  m1p1sr  10516  m1m1sr  10517  mulgt0sr  10529  addcnsrec  10567  mulcnsrec  10568  axmulcom  10579  axmulass  10581  axdistr  10582  axi2m1  10583  addid1  10822  3t3e9  11807  8th4div3  11860  halfpm6th  11861  numma  12145  decmul10add  12170  4t3lem  12198  9t11e99  12231  halfthird  12244  5recm6rec  12245  fz0to3un2pr  13012  seqfeq4  13422  seqof  13430  sqdivi  13551  sq4e2t8  13565  i4  13570  binom2i  13577  nn0opthlem1  13631  facp1  13641  fac2  13642  fac3  13643  fac4  13644  faclbnd4lem1  13656  4bc2eq6  13692  ccat2s1len  13979  ccat2s1lenOLD  13980  ccat2s1p2  13988  ccat2s1p2OLD  13990  cats1len  14224  cats2cat  14226  ofs2  14333  cji  14520  sqrlem5  14608  fsumadd  15098  fsumsplitf  15100  fsumsplitsnun  15112  0.999...  15239  fprodmul  15316  fproddiv  15317  fprodsplitf  15344  bpoly3  15414  fsumcube  15416  efsep  15465  ef01bndlem  15539  cos2bnd  15543  rpnnen2lem3  15571  3dvds2dec  15684  flodddiv4  15766  sadeq  15823  gcdaddmlem  15874  bezout  15893  nn0gcdsq  16094  pythagtriplem16  16169  4sqlem19  16301  dec5nprm  16404  dec2nprm  16405  mod2xnegi  16409  numexp2x  16417  decsplit  16421  karatsuba  16422  2exp16  16426  37prm  16456  43prm  16457  83prm  16458  139prm  16459  163prm  16460  317prm  16461  631prm  16462  1259lem1  16466  1259lem2  16467  1259lem3  16468  1259lem4  16469  1259lem5  16470  1259prm  16471  2503lem1  16472  2503lem2  16473  2503lem3  16474  2503prm  16475  4001lem1  16476  4001lem2  16477  4001lem3  16478  4001lem4  16479  4001prm  16480  funcoppc  17147  estrchom  17379  funcestrcsetclem5  17396  yonedalem3b  17531  symgressbas  18512  gsum2dlem2  19093  opprring  19383  isrhm  19475  evlsval  20301  mamudi  21014  mamudir  21015  oftpos  21063  mamutpos  21069  mdetrlin  21213  mdetrlin2  21218  mdetunilem5  21227  cpmadugsumfi  21487  cnmpt2res  22287  ussval  22870  icopnfhmeo  23549  iccpnfhmeo  23551  pcoass  23630  ovolunlem1a  24099  ioombl1lem3  24163  ioombl1lem4  24164  mbfimaopnlem  24258  itgfsum  24429  iblabslem  24430  itgsplit  24438  dveflem  24578  efhalfpi  25059  efipi  25061  sin2pi  25063  ef2pi  25065  sincosq3sgn  25088  sincosq4sgn  25089  sinq34lt0t  25097  sincos4thpi  25101  tan4thpi  25102  sincos6thpi  25103  sincos3rdpi  25104  pigt3  25105  pige3ALT  25107  cxpcn3  25331  lawcos  25396  1cubrlem  25421  quart1lem  25435  quart1  25436  asin1  25474  atancj  25490  atanlogsublem  25495  log2cnv  25524  log2tlbnd  25525  log2ublem3  25528  log2ub  25529  birthday  25534  basellem8  25667  basellem9  25668  cht2  25751  cht3  25752  1sgm2ppw  25778  bclbnd  25858  bposlem8  25869  bposlem9  25870  lgsdi  25912  lgsquadlem1  25958  2lgsoddprmlem3c  25990  2lgsoddprmlem3d  25991  addsqnreup  26021  mirauto  26472  axsegconlem9  26713  ax5seglem7  26723  vtxdginducedm1  27327  clwlkclwwlkfo  27789  eupth2eucrct  27998  ex-exp  28231  ex-fac  28232  ex-bc  28233  ex-hash  28234  ip0i  28604  ip1ilem  28605  ip2i  28607  ipdirilem  28608  ipasslem10  28618  ip2dii  28623  pythi  28629  siilem1  28630  hvsubsub4i  28838  hvsubcan2i  28843  hisubcomi  28883  normlem0  28888  normlem1  28889  normlem2  28890  normlem3  28891  normlem6  28894  normlem8  28896  normlem9  28897  bcseqi  28899  norm-ii-i  28916  norm-iii-i  28918  normpythi  28921  norm3difi  28926  normpari  28933  normpar2i  28935  polid2i  28936  polidi  28937  bcsiALT  28958  lediri  29316  h1de2i  29332  cmcmlem  29370  cmbr2i  29375  cm2j  29399  fh3i  29402  fh4i  29403  pjaddii  29454  pjsslem  29458  pjssmii  29460  pjdifnormii  29462  lnopeq0lem1  29784  lnopunilem1  29789  lnophmlem2  29796  pjsdi2i  29936  pjclem1  29974  golem1  30050  dpmul100  30575  dpmul1000  30577  dpadd2  30588  dpadd  30589  dpadd3  30590  dpmul  30591  dpmul4  30592  gsumle  30727  matdim  31015  rmulccn  31173  raddcn  31174  xrmulc1cn  31175  xrge0iifhmeo  31181  qqh0  31227  qqh1  31228  elmbfmvol2  31527  mbfmcnt  31528  eulerpartlemgvv  31636  eulerpartlemgh  31638  fib2  31662  fib3  31663  fib4  31664  fib5  31665  fib6  31666  ballotlem2  31748  ballotlemfval0  31755  ballotth  31797  hgt750lem2  31925  problem2  32911  problem4  32913  quad3  32915  poimirlem30  34924  iblabsnclem  34957  dalem10  36811  cdleme0e  37355  cdleme7c  37383  cdleme20c  37449  sn-1ne2  39165  sqmid3api  39176  sqdeccom12  39182  sq3deccom12  39183  nn0expgcd  39191  sn-0lt1  39253  mzpcompact2lem  39355  pellexlem5  39437  pellfundgt1  39487  jm2.27c  39611  areaquad  39830  lhe4.4ex1a  40668  mccl  41886  dvnprodlem2  42239  itgsin0pilem1  42242  stoweidlem13  42305  wallispilem4  42360  wallispi2lem1  42363  wallispi2lem2  42364  dirkerper  42388  dirkertrigeqlem1  42390  fourierdlem30  42429  fourierdlem47  42445  fourierdlem103  42501  fourierdlem104  42502  fouriersw  42523  etransclem37  42563  sge0splitmpt  42700  sge0xaddlem2  42723  sge0xadd  42724  caragen0  42795  caragenuncllem  42801  fsumsplitsndif  43540  2exp5  43762  139prmALT  43766  127prm  43770  2exp11  43772  m11nprm  43773  3exp4mod41  43788  sbgoldbo  43959  2t6m3t4e0  44403  lincsum  44491  zlmodzxzequa  44558  zlmodzxzequap  44561  zlmodzxzldeplem3  44564  rrx2linest  44736  line2  44746  itsclc0yqsollem1  44756  itsclquadb  44770  itscnhlinecirc02plem2  44777