Theorem oveq12i 7374

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

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

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 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-iota 6453  df-fv 6509  df-ov 7365

This theorem is referenced by:  oveq123i  7376  caovdir  7593  caovdilem  7594  caovlem2  7595  cnfcom2  9647  canthwelem  10595  adderpqlem  10899  addassnq  10903  distrnq  10906  ltanq  10916  1lt2nq  10918  ltexnq  10920  halfnq  10921  mulcmpblnrlem  11015  mulcomsr  11034  distrsr  11036  m1p1sr  11037  m1m1sr  11038  mulgt0sr  11050  addcnsrec  11088  mulcnsrec  11089  axmulcom  11100  axmulass  11102  axdistr  11103  axi2m1  11104  addrid  11344  3t3e9  12329  8th4div3  12382  halfpm6th  12383  numma  12671  decmul10add  12696  4t3lem  12724  9t11e99  12757  halfthird  12770  5recm6rec  12771  fz0to3un2pr  13553  seqfeq4  13967  seqof  13975  sqdivi  14099  sq4e2t8  14113  i4  14118  binom2i  14126  nn0opthlem1  14178  facp1  14188  fac2  14189  fac3  14190  fac4  14191  faclbnd4lem1  14203  4bc2eq6  14239  ccat2s1len  14523  ccat2s1p2  14530  cats1len  14761  cats2cat  14763  ofs2  14868  cji  15056  01sqrexlem5  15143  fsumadd  15636  fsumsplitf  15638  fsumsplitsnun  15651  0.999...  15777  fprodmul  15854  fproddiv  15855  fprodsplitf  15882  bpoly3  15952  fsumcube  15954  efsep  16003  ef01bndlem  16077  cos2bnd  16081  rpnnen2lem3  16109  3dvds2dec  16226  flodddiv4  16306  sadeq  16363  gcdaddmlem  16415  bezout  16435  nn0gcdsq  16638  pythagtriplem16  16713  4sqlem19  16846  dec5nprm  16949  dec2nprm  16950  mod2xnegi  16954  numexp2x  16962  decsplit  16966  karatsuba  16967  2exp5  16969  2exp11  16973  2exp16  16974  37prm  17004  43prm  17005  83prm  17006  139prm  17007  163prm  17008  317prm  17009  631prm  17010  1259lem1  17014  1259lem2  17015  1259lem3  17016  1259lem4  17017  1259lem5  17018  1259prm  17019  2503lem1  17020  2503lem2  17021  2503lem3  17022  2503prm  17023  4001lem1  17024  4001lem2  17025  4001lem3  17026  4001lem4  17027  4001prm  17028  funcoppc  17775  estrchom  18028  funcestrcsetclem5  18046  yonedalem3b  18182  symgressbas  19177  gsum2dlem2  19762  opprring  20074  isrhm  20168  evlsval  21533  mamudi  21787  mamudir  21788  oftpos  21838  mamutpos  21844  mdetrlin  21988  mdetrlin2  21993  mdetunilem5  22002  cpmadugsumfi  22263  cnmpt2res  23065  ussval  23648  icopnfhmeo  24343  iccpnfhmeo  24345  pcoass  24424  ovolunlem1a  24897  ioombl1lem3  24961  ioombl1lem4  24962  mbfimaopnlem  25056  itgfsum  25228  iblabslem  25229  itgsplit  25237  dveflem  25380  efhalfpi  25865  efipi  25867  sin2pi  25869  ef2pi  25871  sincosq3sgn  25894  sincosq4sgn  25895  sinq34lt0t  25903  sincos4thpi  25907  tan4thpi  25908  sincos6thpi  25909  sincos3rdpi  25910  pigt3  25911  pige3ALT  25913  cxpcn3  26138  lawcos  26203  1cubrlem  26228  quart1lem  26242  quart1  26243  asin1  26281  atancj  26297  atanlogsublem  26302  log2cnv  26331  log2tlbnd  26332  log2ublem3  26335  log2ub  26336  birthday  26341  basellem8  26474  basellem9  26475  cht2  26558  cht3  26559  1sgm2ppw  26585  bclbnd  26665  bposlem8  26676  bposlem9  26677  lgsdi  26719  lgsquadlem1  26765  2lgsoddprmlem3c  26797  2lgsoddprmlem3d  26798  addsqnreup  26828  addsval2  27318  addsasslem1  27354  addsasslem2  27355  negsval  27367  negs0s  27368  negsid  27382  muls01  27418  muls02  27419  mulsproplem2  27423  mulsproplem3  27424  mulsproplem4  27425  mulsproplem5  27426  mirauto  27689  axsegconlem9  27937  ax5seglem7  27947  vtxdginducedm1  28554  clwlkclwwlkfo  29016  eupth2eucrct  29224  ex-exp  29457  ex-fac  29458  ex-bc  29459  ex-hash  29460  ip0i  29830  ip1ilem  29831  ip2i  29833  ipdirilem  29834  ipasslem10  29844  ip2dii  29849  pythi  29855  siilem1  29856  hvsubsub4i  30064  hvsubcan2i  30069  hisubcomi  30109  normlem0  30114  normlem1  30115  normlem2  30116  normlem3  30117  normlem6  30120  normlem8  30122  normlem9  30123  bcseqi  30125  norm-ii-i  30142  norm-iii-i  30144  normpythi  30147  norm3difi  30152  normpari  30159  normpar2i  30161  polid2i  30162  polidi  30163  bcsiALT  30184  lediri  30542  h1de2i  30558  cmcmlem  30596  cmbr2i  30601  cm2j  30625  fh3i  30628  fh4i  30629  pjaddii  30680  pjsslem  30684  pjssmii  30686  pjdifnormii  30688  lnopeq0lem1  31010  lnopunilem1  31015  lnophmlem2  31022  pjsdi2i  31162  pjclem1  31200  golem1  31276  dpmul100  31823  dpmul1000  31825  dpadd2  31836  dpadd  31837  dpadd3  31838  dpmul  31839  dpmul4  31840  gsumle  32002  matdim  32397  rmulccn  32598  raddcn  32599  xrmulc1cn  32600  xrge0iifhmeo  32606  qqh0  32654  qqh1  32655  elmbfmvol2  32956  mbfmcnt  32957  eulerpartlemgvv  33065  eulerpartlemgh  33067  fib2  33091  fib3  33092  fib4  33093  fib5  33094  fib6  33095  ballotlem2  33177  ballotlemfval0  33184  ballotth  33226  hgt750lem2  33354  problem2  34341  problem4  34343  quad3  34345  poimirlem30  36181  iblabsnclem  36214  dalem10  38209  cdleme0e  38753  cdleme7c  38781  cdleme20c  38847  3exp7  40583  3lexlogpow5ineq1  40584  3lexlogpow5ineq5  40590  aks4d1p1  40606  5bc2eq10  40623  sn-1ne2  40839  sqmid3api  40855  sqdeccom12  40861  sq3deccom12  40862  nn0expgcd  40879  rei4  40950  ipiiie0  40964  sn-0tie0  40966  mzpcompact2lem  41132  pellexlem5  41214  pellfundgt1  41264  jm2.27c  41389  areaquad  41608  resqrtvalex  42039  imsqrtvalex  42040  lhe4.4ex1a  42731  mccl  43959  dvnprodlem2  44308  itgsin0pilem1  44311  stoweidlem13  44374  wallispilem4  44429  wallispi2lem1  44432  wallispi2lem2  44433  dirkerper  44457  dirkertrigeqlem1  44459  fourierdlem30  44498  fourierdlem47  44514  fourierdlem103  44570  fourierdlem104  44571  fouriersw  44592  etransclem37  44632  sge0splitmpt  44772  sge0xaddlem2  44795  sge0xadd  44796  caragen0  44867  caragenuncllem  44873  fsumsplitsndif  45685  139prmALT  45908  127prm  45911  m11nprm  45913  3exp4mod41  45928  sbgoldbo  46099  2t6m3t4e0  46544  lincsum  46630  zlmodzxzequa  46697  zlmodzxzequap  46700  zlmodzxzldeplem3  46703  rrx2linest  46948  line2  46958  itsclc0yqsollem1  46968  itsclquadb  46982  itscnhlinecirc02plem2  46989