Theorem oveq12i 7422

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

This proof depends on syntax axioms:   = wceq 1570  (class class class)co 7410

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-ov 7413

This theorem is used by:  oveq123i  7424  caovdir  7644  caovdilem  7645  caovlem2  7646  cnfcom2  9667  canthwelem  10639  adderpqlem  10943  addassnq  10947  distrnq  10950  ltanq  10960  1lt2nq  10962  ltexnq  10964  halfnq  10965  mulcmpblnrlem  11059  mulcomsr  11078  distrsr  11080  m1p1sr  11081  m1m1sr  11082  mulgt0sr  11094  addcnsrec  11132  mulcnsrec  11133  axmulcom  11144  axmulass  11146  axdistr  11147  axi2m1  11148  addrid  11394  3t3e9  12412  8th4div3  12468  halfthird  12469  numma  12764  decmul10add  12789  4t3lem  12817  9t11e99OLD  12851  5recm6rec  12865  fz0to3un2pr  13662  seqfeq4  14092  seqof  14100  sqdivi  14226  sq4e2t8  14240  i4  14245  binom2i  14253  nn0opthlem1  14309  facp1  14319  fac2  14320  fac3  14321  fac4  14322  faclbnd4lem1  14334  4bc2eq6  14370  ccat2s1len  14666  ccat2s1p2  14673  cats1len  14902  cats2cat  14904  ofs2  15013  cji  15215  01sqrexlem5  15302  fsumadd  15796  fsumsplitf  15798  fsumsplitsnun  15811  0.999...  15940  fprodmul  16019  fproddiv  16020  fprodsplitf  16047  bpoly3  16116  fsumcube  16118  efsep  16170  ef01bndlem  16244  cos2bnd  16248  rpnnen2lem3  16276  3dvds2dec  16395  flodddiv4  16477  sadeq  16534  gcdaddmlem  16586  bezout  16605  nn0expgcd  16626  nn0gcdsq  16815  pythagtriplem16  16894  4sqlem19  17027  dec5nprm  17130  dec2nprm  17131  mod2xnegi  17135  numexp2x  17142  decsplit  17146  karatsuba  17147  2exp5  17149  2exp11  17153  2exp16  17154  37prm  17185  43prm  17186  83prm  17187  139prm  17188  163prm  17189  317prm  17190  631prm  17191  1259lem1  17195  1259lem2  17196  1259lem3  17197  1259lem4  17198  1259lem5  17199  1259prm  17200  2503lem1  17201  2503lem2  17202  2503lem3  17203  2503prm  17204  4001lem1  17205  4001lem2  17206  4001lem3  17207  4001lem4  17208  4001prm  17209  funcoppc  17936  estrchom  18187  funcestrcsetclem5  18204  yonedalem3b  18339  ecqusaddd  19267  symgressbas  19456  gsum2dlem2  20045  gsumle  20219  opprrng  20432  isrhm  20566  rngqiprnglinlem2  21441  pzriprng1ALT  21655  evlsval  22246  mamudi  22569  mamudir  22570  oftpos  22618  mamutpos  22624  mdetrlin  22768  mdetrlin2  22773  mdetunilem5  22782  cpmadugsumfi  23043  cnmpt2res  23843  ussval  24425  icopnfhmeo  25111  iccpnfhmeo  25113  pcoass  25192  ovolunlem1a  25664  ioombl1lem3  25728  ioombl1lem4  25729  mbfimaopnlem  25823  itgfsum  25995  iblabslem  25996  itgsplit  26004  dveflem  26147  efhalfpi  26645  efipi  26647  sin2pi  26649  ef2pi  26651  sincosq3sgn  26674  sincosq4sgn  26675  sinq34lt0t  26683  sincos4thpi  26687  tan4thpi  26688  tan4thpiOLD  26689  sincos6thpi  26690  sincos3rdpi  26691  pigt3  26692  pige3ALT  26694  cxpcn3  26922  lawcos  26990  1cubrlem  27015  quart1lem  27029  quart1  27030  asin1  27068  atancj  27084  atanlogsublem  27089  log2cnv  27118  log2tlbnd  27119  log2ublem3  27122  log2ub  27123  birthday  27128  basellem8  27261  basellem9  27262  cht2  27345  cht3  27346  1sgm2ppw  27373  bclbnd  27453  bposlem8  27464  bposlem9  27465  lgsdi  27507  lgsquadlem1  27553  2lgsoddprmlem3c  27585  2lgsoddprmlem3d  27586  addsqnreup  27616  addsval2  28165  addsunif  28204  addsasslem1  28205  addsasslem2  28206  negsval  28227  neg0s  28228  neg1s  28229  negsid  28243  mulsval2  28313  muls01  28314  mulsproplem2  28319  mulsproplem3  28320  mulsproplem4  28321  mulsproplem5  28322  mulsproplem6  28323  mulsproplem7  28324  mulsproplem8  28325  mulsproplem12  28329  mulsproplem13  28330  mulsproplem14  28331  mulsunif  28352  addsdilem1  28353  addsdilem2  28354  mulsasslem1  28365  mulsasslem2  28366  mulsunif2  28372  precsexlem11  28419  onmulscl  28480  twocut  28625  mirauto  28970  axsegconlem9  29284  ax5seglem7  29294  vtxdginducedm1  29902  clwlkclwwlkfo  30369  eupth2eucrct  30577  ex-exp  30810  ex-fac  30811  ex-bc  30812  ex-hash  30813  ip0i  31186  ip1ilem  31187  ip2i  31189  ipdirilem  31190  ipasslem10  31200  ip2dii  31205  pythi  31211  siilem1  31212  hvsubsub4i  31420  hvsubcan2i  31425  hisubcomi  31465  normlem0  31470  normlem1  31471  normlem2  31472  normlem3  31473  normlem6  31476  normlem8  31478  normlem9  31479  bcseqi  31481  norm-ii-i  31498  norm-iii-i  31500  normpythi  31503  norm3difi  31508  normpari  31515  normpar2i  31517  polid2i  31518  polidi  31519  bcsiALT  31540  lediri  31898  h1de2i  31914  cmcmlem  31952  cmbr2i  31957  cm2j  31981  fh3i  31984  fh4i  31985  pjaddii  32036  pjsslem  32040  pjssmii  32042  pjdifnormii  32044  lnopeq0lem1  32366  lnopunilem1  32371  lnophmlem2  32378  pjsdi2i  32518  pjclem1  32556  golem1  32632  dpmul100  33225  dpmul1000  33227  dpadd2  33238  dpadd  33239  dpadd3  33240  dpmul  33241  dpmul4  33242  ccatws1f1o  33280  elrgspnlem2  33572  matdim  34014  fldext2chn  34127  constrextdg2lem  34147  constrext2chnlem  34149  iconstr  34165  cos9thpiminplylem4  34184  cos9thpiminplylem5  34185  rmulccn  34327  raddcn  34328  xrmulc1cn  34329  xrge0iifhmeo  34335  qqh0  34383  qqh1  34384  elmbfmvol2  34666  mbfmcnt  34667  eulerpartlemgvv  34775  eulerpartlemgh  34777  fib2  34801  fib3  34802  fib4  34803  fib5  34804  fib6  34805  ballotlem2  34888  ballotlemfval0  34895  ballotth  34937  hgt750lem2  35048  problem2  36166  problem4  36168  quad3  36170  ditgeq123i  36749  cbvditgvw2  36789  poimirlem30  38329  iblabsnclem  38362  dalem10  40475  cdleme0e  41019  cdleme7c  41047  cdleme20c  41113  3exp7  42848  3lexlogpow5ineq1  42849  3lexlogpow5ineq5  42855  aks4d1p1  42871  5bc2eq10  42937  aks5lem3a  42984  25or6to4  43001  sn-1ne2  43060  sqmid3api  43072  sqdeccom12  43078  sq3deccom12  43079  tan3rdpi  43141  sin2t3rdpi  43142  cos2t3rdpi  43143  rei4  43213  ipiiie0  43227  sn-0tie0  43253  mzpcompact2lem  43510  pellexlem5  43588  pellfundgt1  43638  jm2.27c  43762  areaquad  43971  resqrtvalex  44399  imsqrtvalex  44400  lhe4.4ex1a  45067  mccl  46342  dvnprodlem2  46689  itgsin0pilem1  46692  stoweidlem13  46755  wallispilem4  46810  wallispi2lem1  46813  wallispi2lem2  46814  dirkerper  46838  dirkertrigeqlem1  46840  fourierdlem30  46879  fourierdlem47  46895  fourierdlem103  46951  fourierdlem104  46952  fouriersw  46973  etransclem37  47013  sge0splitmpt  47153  sge0xaddlem2  47176  sge0xadd  47177  caragen0  47248  caragenuncllem  47254  goldrasin  47647  goldratmolem2  47651  fsumsplitsndif  48146  139prmALT  48376  127prm  48379  m11nprm  48381  3exp4mod41  48396  ppivalnn4  48407  sbgoldbo  48580  2t6m3t4e0  49156  lincsum  49237  zlmodzxzequa  49304  zlmodzxzequap  49307  zlmodzxzldeplem3  49310  rrx2linest  49550  line2  49560  itsclc0yqsollem1  49570  itsclquadb  49584  itscnhlinecirc02plem2  49591  postcofval  50170  postcofcl  50171  precofval  50173  precofvalALT  50174  precofcl  50176  termcfuncval  50338  crosspdoti  50674  crossp3i  50676