Theorem oveq12i 7354

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

Syntax hints:   = wceq 1541  (class class class)co 7342

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3405  df-v 3444  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4275  df-if 4479  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4858  df-br 5098  df-iota 6436  df-fv 6492  df-ov 7345

This theorem is referenced by:  oveq123i  7356  caovdir  7573  caovdilem  7574  caovlem2  7575  cnfcom2  9564  canthwelem  10512  adderpqlem  10816  addassnq  10820  distrnq  10823  ltanq  10833  1lt2nq  10835  ltexnq  10837  halfnq  10838  mulcmpblnrlem  10932  mulcomsr  10951  distrsr  10953  m1p1sr  10954  m1m1sr  10955  mulgt0sr  10967  addcnsrec  11005  mulcnsrec  11006  axmulcom  11017  axmulass  11019  axdistr  11020  axi2m1  11021  addid1  11261  3t3e9  12246  8th4div3  12299  halfpm6th  12300  numma  12587  decmul10add  12612  4t3lem  12640  9t11e99  12673  halfthird  12686  5recm6rec  12687  fz0to3un2pr  13464  seqfeq4  13878  seqof  13886  sqdivi  14008  sq4e2t8  14022  i4  14027  binom2i  14034  nn0opthlem1  14088  facp1  14098  fac2  14099  fac3  14100  fac4  14101  faclbnd4lem1  14113  4bc2eq6  14149  ccat2s1len  14431  ccat2s1p2  14438  cats1len  14673  cats2cat  14675  ofs2  14782  cji  14970  sqrlem5  15058  fsumadd  15552  fsumsplitf  15554  fsumsplitsnun  15567  0.999...  15693  fprodmul  15770  fproddiv  15771  fprodsplitf  15798  bpoly3  15868  fsumcube  15870  efsep  15919  ef01bndlem  15993  cos2bnd  15997  rpnnen2lem3  16025  3dvds2dec  16142  flodddiv4  16222  sadeq  16279  gcdaddmlem  16331  bezout  16351  nn0gcdsq  16554  pythagtriplem16  16629  4sqlem19  16762  dec5nprm  16865  dec2nprm  16866  mod2xnegi  16870  numexp2x  16878  decsplit  16882  karatsuba  16883  2exp5  16885  2exp11  16889  2exp16  16890  37prm  16920  43prm  16921  83prm  16922  139prm  16923  163prm  16924  317prm  16925  631prm  16926  1259lem1  16930  1259lem2  16931  1259lem3  16932  1259lem4  16933  1259lem5  16934  1259prm  16935  2503lem1  16936  2503lem2  16937  2503lem3  16938  2503prm  16939  4001lem1  16940  4001lem2  16941  4001lem3  16942  4001lem4  16943  4001prm  16944  funcoppc  17688  estrchom  17941  funcestrcsetclem5  17959  yonedalem3b  18095  symgressbas  19086  gsum2dlem2  19667  opprring  19968  isrhm  20060  evlsval  21402  mamudi  21656  mamudir  21657  oftpos  21707  mamutpos  21713  mdetrlin  21857  mdetrlin2  21862  mdetunilem5  21871  cpmadugsumfi  22132  cnmpt2res  22934  ussval  23517  icopnfhmeo  24212  iccpnfhmeo  24214  pcoass  24293  ovolunlem1a  24766  ioombl1lem3  24830  ioombl1lem4  24831  mbfimaopnlem  24925  itgfsum  25097  iblabslem  25098  itgsplit  25106  dveflem  25249  efhalfpi  25734  efipi  25736  sin2pi  25738  ef2pi  25740  sincosq3sgn  25763  sincosq4sgn  25764  sinq34lt0t  25772  sincos4thpi  25776  tan4thpi  25777  sincos6thpi  25778  sincos3rdpi  25779  pigt3  25780  pige3ALT  25782  cxpcn3  26007  lawcos  26072  1cubrlem  26097  quart1lem  26111  quart1  26112  asin1  26150  atancj  26166  atanlogsublem  26171  log2cnv  26200  log2tlbnd  26201  log2ublem3  26204  log2ub  26205  birthday  26210  basellem8  26343  basellem9  26344  cht2  26427  cht3  26428  1sgm2ppw  26454  bclbnd  26534  bposlem8  26545  bposlem9  26546  lgsdi  26588  lgsquadlem1  26634  2lgsoddprmlem3c  26666  2lgsoddprmlem3d  26667  addsqnreup  26697  mirauto  27334  axsegconlem9  27582  ax5seglem7  27592  vtxdginducedm1  28199  clwlkclwwlkfo  28661  eupth2eucrct  28869  ex-exp  29102  ex-fac  29103  ex-bc  29104  ex-hash  29105  ip0i  29475  ip1ilem  29476  ip2i  29478  ipdirilem  29479  ipasslem10  29489  ip2dii  29494  pythi  29500  siilem1  29501  hvsubsub4i  29709  hvsubcan2i  29714  hisubcomi  29754  normlem0  29759  normlem1  29760  normlem2  29761  normlem3  29762  normlem6  29765  normlem8  29767  normlem9  29768  bcseqi  29770  norm-ii-i  29787  norm-iii-i  29789  normpythi  29792  norm3difi  29797  normpari  29804  normpar2i  29806  polid2i  29807  polidi  29808  bcsiALT  29829  lediri  30187  h1de2i  30203  cmcmlem  30241  cmbr2i  30246  cm2j  30270  fh3i  30273  fh4i  30274  pjaddii  30325  pjsslem  30329  pjssmii  30331  pjdifnormii  30333  lnopeq0lem1  30655  lnopunilem1  30660  lnophmlem2  30667  pjsdi2i  30807  pjclem1  30845  golem1  30921  dpmul100  31456  dpmul1000  31458  dpadd2  31469  dpadd  31470  dpadd3  31471  dpmul  31472  dpmul4  31473  gsumle  31635  matdim  31994  rmulccn  32174  raddcn  32175  xrmulc1cn  32176  xrge0iifhmeo  32182  qqh0  32230  qqh1  32231  elmbfmvol2  32532  mbfmcnt  32533  eulerpartlemgvv  32641  eulerpartlemgh  32643  fib2  32667  fib3  32668  fib4  32669  fib5  32670  fib6  32671  ballotlem2  32753  ballotlemfval0  32760  ballotth  32802  hgt750lem2  32930  problem2  33921  problem4  33923  quad3  33925  addsval2  34228  addsasslem1  34257  addsasslem2  34258  negsval  34267  negs0s  34268  poimirlem30  35961  iblabsnclem  35994  dalem10  37990  cdleme0e  38534  cdleme7c  38562  cdleme20c  38628  3exp7  40364  3lexlogpow5ineq1  40365  3lexlogpow5ineq5  40371  aks4d1p1  40387  5bc2eq10  40404  sn-1ne2  40604  sqmid3api  40620  sqdeccom12  40626  sq3deccom12  40627  nn0expgcd  40644  rei4  40714  ipiiie0  40728  sn-0tie0  40730  sn-0lt1  40741  mzpcompact2lem  40884  pellexlem5  40966  pellfundgt1  41016  jm2.27c  41141  areaquad  41360  resqrtvalex  41624  imsqrtvalex  41625  lhe4.4ex1a  42318  mccl  43525  dvnprodlem2  43874  itgsin0pilem1  43877  stoweidlem13  43940  wallispilem4  43995  wallispi2lem1  43998  wallispi2lem2  43999  dirkerper  44023  dirkertrigeqlem1  44025  fourierdlem30  44064  fourierdlem47  44080  fourierdlem103  44136  fourierdlem104  44137  fouriersw  44158  etransclem37  44198  sge0splitmpt  44336  sge0xaddlem2  44359  sge0xadd  44360  caragen0  44431  caragenuncllem  44437  fsumsplitsndif  45241  139prmALT  45464  127prm  45467  m11nprm  45469  3exp4mod41  45484  sbgoldbo  45655  2t6m3t4e0  46100  lincsum  46186  zlmodzxzequa  46253  zlmodzxzequap  46256  zlmodzxzldeplem3  46259  rrx2linest  46504  line2  46514  itsclc0yqsollem1  46524  itsclquadb  46538  itscnhlinecirc02plem2  46545