Theorem oveq12i 7162

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

Syntax hints:   = wceq 1533  (class class class)co 7150

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rex 3144  df-rab 3147  df-v 3497  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4833  df-br 5060  df-iota 6309  df-fv 6358  df-ov 7153

This theorem is referenced by:  oveq123i  7164  caovdir  7376  caovdilem  7377  caovlem2  7378  cnfcom2  9159  canthwelem  10066  adderpqlem  10370  addassnq  10374  distrnq  10377  ltanq  10387  1lt2nq  10389  ltexnq  10391  halfnq  10392  mulcmpblnrlem  10486  mulcomsr  10505  distrsr  10507  m1p1sr  10508  m1m1sr  10509  mulgt0sr  10521  addcnsrec  10559  mulcnsrec  10560  axmulcom  10571  axmulass  10573  axdistr  10574  axi2m1  10575  addid1  10814  3t3e9  11798  8th4div3  11851  halfpm6th  11852  numma  12136  decmul10add  12161  4t3lem  12189  9t11e99  12222  halfthird  12235  5recm6rec  12236  fz0to3un2pr  13003  seqfeq4  13413  seqof  13421  sqdivi  13542  sq4e2t8  13556  i4  13561  binom2i  13568  nn0opthlem1  13622  facp1  13632  fac2  13633  fac3  13634  fac4  13635  faclbnd4lem1  13647  4bc2eq6  13683  ccat2s1len  13971  ccat2s1lenOLD  13972  ccat2s1p2  13980  ccat2s1p2OLD  13982  cats1len  14216  cats2cat  14218  ofs2  14325  cji  14512  sqrlem5  14600  fsumadd  15090  fsumsplitf  15092  fsumsplitsnun  15104  0.999...  15231  fprodmul  15308  fproddiv  15309  fprodsplitf  15336  bpoly3  15406  fsumcube  15408  efsep  15457  ef01bndlem  15531  cos2bnd  15535  rpnnen2lem3  15563  3dvds2dec  15676  flodddiv4  15758  sadeq  15815  gcdaddmlem  15866  bezout  15885  nn0gcdsq  16086  pythagtriplem16  16161  4sqlem19  16293  dec5nprm  16396  dec2nprm  16397  mod2xnegi  16401  numexp2x  16409  decsplit  16413  karatsuba  16414  2exp16  16418  37prm  16448  43prm  16449  83prm  16450  139prm  16451  163prm  16452  317prm  16453  631prm  16454  1259lem1  16458  1259lem2  16459  1259lem3  16460  1259lem4  16461  1259lem5  16462  1259prm  16463  2503lem1  16464  2503lem2  16465  2503lem3  16466  2503prm  16467  4001lem1  16468  4001lem2  16469  4001lem3  16470  4001lem4  16471  4001prm  16472  funcoppc  17139  estrchom  17371  funcestrcsetclem5  17388  yonedalem3b  17523  symgressbas  18504  gsum2dlem2  19085  opprring  19375  isrhm  19467  evlsval  20293  mamudi  21006  mamudir  21007  oftpos  21055  mamutpos  21061  mdetrlin  21205  mdetrlin2  21210  mdetunilem5  21219  cpmadugsumfi  21479  cnmpt2res  22279  ussval  22862  icopnfhmeo  23541  iccpnfhmeo  23543  pcoass  23622  ovolunlem1a  24091  ioombl1lem3  24155  ioombl1lem4  24156  mbfimaopnlem  24250  itgfsum  24421  iblabslem  24422  itgsplit  24430  dveflem  24570  efhalfpi  25051  efipi  25053  sin2pi  25055  ef2pi  25057  sincosq3sgn  25080  sincosq4sgn  25081  sinq34lt0t  25089  sincos4thpi  25093  tan4thpi  25094  sincos6thpi  25095  sincos3rdpi  25096  pigt3  25097  pige3ALT  25099  cxpcn3  25323  lawcos  25388  1cubrlem  25413  quart1lem  25427  quart1  25428  asin1  25466  atancj  25482  atanlogsublem  25487  log2cnv  25516  log2tlbnd  25517  log2ublem3  25520  log2ub  25521  birthday  25526  basellem8  25659  basellem9  25660  cht2  25743  cht3  25744  1sgm2ppw  25770  bclbnd  25850  bposlem8  25861  bposlem9  25862  lgsdi  25904  lgsquadlem1  25950  2lgsoddprmlem3c  25982  2lgsoddprmlem3d  25983  addsqnreup  26013  mirauto  26464  axsegconlem9  26705  ax5seglem7  26715  vtxdginducedm1  27319  clwlkclwwlkfo  27781  eupth2eucrct  27990  ex-exp  28223  ex-fac  28224  ex-bc  28225  ex-hash  28226  ip0i  28596  ip1ilem  28597  ip2i  28599  ipdirilem  28600  ipasslem10  28610  ip2dii  28615  pythi  28621  siilem1  28622  hvsubsub4i  28830  hvsubcan2i  28835  hisubcomi  28875  normlem0  28880  normlem1  28881  normlem2  28882  normlem3  28883  normlem6  28886  normlem8  28888  normlem9  28889  bcseqi  28891  norm-ii-i  28908  norm-iii-i  28910  normpythi  28913  norm3difi  28918  normpari  28925  normpar2i  28927  polid2i  28928  polidi  28929  bcsiALT  28950  lediri  29308  h1de2i  29324  cmcmlem  29362  cmbr2i  29367  cm2j  29391  fh3i  29394  fh4i  29395  pjaddii  29446  pjsslem  29450  pjssmii  29452  pjdifnormii  29454  lnopeq0lem1  29776  lnopunilem1  29781  lnophmlem2  29788  pjsdi2i  29928  pjclem1  29966  golem1  30042  dpmul100  30568  dpmul1000  30570  dpadd2  30581  dpadd  30582  dpadd3  30583  dpmul  30584  dpmul4  30585  gsumle  30720  matdim  31008  rmulccn  31166  raddcn  31167  xrmulc1cn  31168  xrge0iifhmeo  31174  qqh0  31220  qqh1  31221  elmbfmvol2  31520  mbfmcnt  31521  eulerpartlemgvv  31629  eulerpartlemgh  31631  fib2  31655  fib3  31656  fib4  31657  fib5  31658  fib6  31659  ballotlem2  31741  ballotlemfval0  31748  ballotth  31790  hgt750lem2  31918  problem2  32904  problem4  32906  quad3  32908  poimirlem30  34916  iblabsnclem  34949  dalem10  36803  cdleme0e  37347  cdleme7c  37375  cdleme20c  37441  sn-1ne2  39151  sqmid3api  39162  sqdeccom12  39168  sq3deccom12  39169  nn0expgcd  39177  sn-0lt1  39239  mzpcompact2lem  39341  pellexlem5  39423  pellfundgt1  39473  jm2.27c  39597  areaquad  39816  lhe4.4ex1a  40654  mccl  41871  dvnprodlem2  42224  itgsin0pilem1  42227  stoweidlem13  42291  wallispilem4  42346  wallispi2lem1  42349  wallispi2lem2  42350  dirkerper  42374  dirkertrigeqlem1  42376  fourierdlem30  42415  fourierdlem47  42431  fourierdlem103  42487  fourierdlem104  42488  fouriersw  42509  etransclem37  42549  sge0splitmpt  42686  sge0xaddlem2  42709  sge0xadd  42710  caragen0  42781  caragenuncllem  42787  fsumsplitsndif  43526  2exp5  43748  139prmALT  43752  127prm  43756  2exp11  43758  m11nprm  43759  3exp4mod41  43774  sbgoldbo  43945  2t6m3t4e0  44389  lincsum  44477  zlmodzxzequa  44544  zlmodzxzequap  44547  zlmodzxzldeplem3  44550  rrx2linest  44722  line2  44732  itsclc0yqsollem1  44742  itsclquadb  44756  itscnhlinecirc02plem2  44763