Theorem oveq12i 7203

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

Syntax hints:   = wceq 1543  (class class class)co 7191

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-iota 6316  df-fv 6366  df-ov 7194

This theorem is referenced by:  oveq123i  7205  caovdir  7420  caovdilem  7421  caovlem2  7422  cnfcom2  9295  canthwelem  10229  adderpqlem  10533  addassnq  10537  distrnq  10540  ltanq  10550  1lt2nq  10552  ltexnq  10554  halfnq  10555  mulcmpblnrlem  10649  mulcomsr  10668  distrsr  10670  m1p1sr  10671  m1m1sr  10672  mulgt0sr  10684  addcnsrec  10722  mulcnsrec  10723  axmulcom  10734  axmulass  10736  axdistr  10737  axi2m1  10738  addid1  10977  3t3e9  11962  8th4div3  12015  halfpm6th  12016  numma  12302  decmul10add  12327  4t3lem  12355  9t11e99  12388  halfthird  12401  5recm6rec  12402  fz0to3un2pr  13179  seqfeq4  13590  seqof  13598  sqdivi  13719  sq4e2t8  13733  i4  13738  binom2i  13745  nn0opthlem1  13799  facp1  13809  fac2  13810  fac3  13811  fac4  13812  faclbnd4lem1  13824  4bc2eq6  13860  ccat2s1len  14145  ccat2s1lenOLD  14146  ccat2s1p2  14154  ccat2s1p2OLD  14156  cats1len  14390  cats2cat  14392  ofs2  14499  cji  14687  sqrlem5  14775  fsumadd  15268  fsumsplitf  15270  fsumsplitsnun  15282  0.999...  15408  fprodmul  15485  fproddiv  15486  fprodsplitf  15513  bpoly3  15583  fsumcube  15585  efsep  15634  ef01bndlem  15708  cos2bnd  15712  rpnnen2lem3  15740  3dvds2dec  15857  flodddiv4  15937  sadeq  15994  gcdaddmlem  16046  bezout  16066  nn0gcdsq  16271  pythagtriplem16  16346  4sqlem19  16479  dec5nprm  16582  dec2nprm  16583  mod2xnegi  16587  numexp2x  16595  decsplit  16599  karatsuba  16600  2exp5  16602  2exp11  16606  2exp16  16607  37prm  16637  43prm  16638  83prm  16639  139prm  16640  163prm  16641  317prm  16642  631prm  16643  1259lem1  16647  1259lem2  16648  1259lem3  16649  1259lem4  16650  1259lem5  16651  1259prm  16652  2503lem1  16653  2503lem2  16654  2503lem3  16655  2503prm  16656  4001lem1  16657  4001lem2  16658  4001lem3  16659  4001lem4  16660  4001prm  16661  funcoppc  17335  estrchom  17588  funcestrcsetclem5  17605  yonedalem3b  17741  symgressbas  18728  gsum2dlem2  19310  opprring  19603  isrhm  19695  evlsval  21000  mamudi  21254  mamudir  21255  oftpos  21303  mamutpos  21309  mdetrlin  21453  mdetrlin2  21458  mdetunilem5  21467  cpmadugsumfi  21728  cnmpt2res  22528  ussval  23111  icopnfhmeo  23794  iccpnfhmeo  23796  pcoass  23875  ovolunlem1a  24347  ioombl1lem3  24411  ioombl1lem4  24412  mbfimaopnlem  24506  itgfsum  24678  iblabslem  24679  itgsplit  24687  dveflem  24830  efhalfpi  25315  efipi  25317  sin2pi  25319  ef2pi  25321  sincosq3sgn  25344  sincosq4sgn  25345  sinq34lt0t  25353  sincos4thpi  25357  tan4thpi  25358  sincos6thpi  25359  sincos3rdpi  25360  pigt3  25361  pige3ALT  25363  cxpcn3  25588  lawcos  25653  1cubrlem  25678  quart1lem  25692  quart1  25693  asin1  25731  atancj  25747  atanlogsublem  25752  log2cnv  25781  log2tlbnd  25782  log2ublem3  25785  log2ub  25786  birthday  25791  basellem8  25924  basellem9  25925  cht2  26008  cht3  26009  1sgm2ppw  26035  bclbnd  26115  bposlem8  26126  bposlem9  26127  lgsdi  26169  lgsquadlem1  26215  2lgsoddprmlem3c  26247  2lgsoddprmlem3d  26248  addsqnreup  26278  mirauto  26729  axsegconlem9  26970  ax5seglem7  26980  vtxdginducedm1  27585  clwlkclwwlkfo  28046  eupth2eucrct  28254  ex-exp  28487  ex-fac  28488  ex-bc  28489  ex-hash  28490  ip0i  28860  ip1ilem  28861  ip2i  28863  ipdirilem  28864  ipasslem10  28874  ip2dii  28879  pythi  28885  siilem1  28886  hvsubsub4i  29094  hvsubcan2i  29099  hisubcomi  29139  normlem0  29144  normlem1  29145  normlem2  29146  normlem3  29147  normlem6  29150  normlem8  29152  normlem9  29153  bcseqi  29155  norm-ii-i  29172  norm-iii-i  29174  normpythi  29177  norm3difi  29182  normpari  29189  normpar2i  29191  polid2i  29192  polidi  29193  bcsiALT  29214  lediri  29572  h1de2i  29588  cmcmlem  29626  cmbr2i  29631  cm2j  29655  fh3i  29658  fh4i  29659  pjaddii  29710  pjsslem  29714  pjssmii  29716  pjdifnormii  29718  lnopeq0lem1  30040  lnopunilem1  30045  lnophmlem2  30052  pjsdi2i  30192  pjclem1  30230  golem1  30306  dpmul100  30845  dpmul1000  30847  dpadd2  30858  dpadd  30859  dpadd3  30860  dpmul  30861  dpmul4  30862  gsumle  31023  matdim  31366  rmulccn  31546  raddcn  31547  xrmulc1cn  31548  xrge0iifhmeo  31554  qqh0  31600  qqh1  31601  elmbfmvol2  31900  mbfmcnt  31901  eulerpartlemgvv  32009  eulerpartlemgh  32011  fib2  32035  fib3  32036  fib4  32037  fib5  32038  fib6  32039  ballotlem2  32121  ballotlemfval0  32128  ballotth  32170  hgt750lem2  32298  problem2  33291  problem4  33293  quad3  33295  negsval  33809  negs0s  33810  poimirlem30  35493  iblabsnclem  35526  dalem10  37373  cdleme0e  37917  cdleme7c  37945  cdleme20c  38011  3exp7  39744  3lexlogpow5ineq1  39745  3lexlogpow5ineq5  39751  aks4d1p1  39766  5bc2eq10  39767  sn-1ne2  39943  sqmid3api  39959  sqdeccom12  39965  sq3deccom12  39966  nn0expgcd  39984  rei4  40054  ipiiie0  40068  sn-0tie0  40070  sn-0lt1  40081  mzpcompact2lem  40217  pellexlem5  40299  pellfundgt1  40349  jm2.27c  40473  areaquad  40691  resqrtvalex  40870  imsqrtvalex  40871  lhe4.4ex1a  41561  mccl  42757  dvnprodlem2  43106  itgsin0pilem1  43109  stoweidlem13  43172  wallispilem4  43227  wallispi2lem1  43230  wallispi2lem2  43231  dirkerper  43255  dirkertrigeqlem1  43257  fourierdlem30  43296  fourierdlem47  43312  fourierdlem103  43368  fourierdlem104  43369  fouriersw  43390  etransclem37  43430  sge0splitmpt  43567  sge0xaddlem2  43590  sge0xadd  43591  caragen0  43662  caragenuncllem  43668  fsumsplitsndif  44441  139prmALT  44664  127prm  44667  m11nprm  44669  3exp4mod41  44684  sbgoldbo  44855  2t6m3t4e0  45300  lincsum  45386  zlmodzxzequa  45453  zlmodzxzequap  45456  zlmodzxzldeplem3  45459  rrx2linest  45704  line2  45714  itsclc0yqsollem1  45724  itsclquadb  45738  itscnhlinecirc02plem2  45745