Theorem oveq12i 7428

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7419

This theorem is used by:  oveq123i  7430  caovdir  7651  caovdilem  7652  caovlem2  7653  cnfcom2  9684  canthwelem  10660  adderpqlem  10964  addassnq  10968  distrnq  10971  ltanq  10981  1lt2nq  10983  ltexnq  10985  halfnq  10986  mulcmpblnrlem  11080  mulcomsr  11099  distrsr  11101  m1p1sr  11102  m1m1sr  11103  mulgt0sr  11115  addcnsrec  11153  mulcnsrec  11154  axmulcom  11165  axmulass  11167  axdistr  11168  axi2m1  11169  addrid  11415  3t3e9  12433  8th4div3  12489  halfthird  12490  numma  12786  decmul10add  12811  4t3lem  12839  9t11e99OLD  12873  5recm6rec  12887  fz0to3un2pr  13684  seqfeq4  14115  seqof  14123  sqdivi  14249  sq4e2t8  14263  i4  14268  binom2i  14276  nn0opthlem1  14332  facp1  14342  fac2  14343  fac3  14344  fac4  14345  faclbnd4lem1  14357  4bc2eq6  14393  ccat2s1len  14691  ccat2s1p2  14698  cats1len  14931  cats2cat  14933  ofs2  15044  cji  15246  01sqrexlem5  15333  fsumadd  15826  fsumsplitf  15828  fsumsplitsnun  15841  0.999...  15970  fprodmul  16049  fproddiv  16050  fprodsplitf  16077  bpoly3  16146  fsumcube  16148  efsep  16200  ef01bndlem  16274  cos2bnd  16278  rpnnen2lem3  16306  3dvds2dec  16425  flodddiv4  16507  sadeq  16564  gcdaddmlem  16616  bezout  16635  nn0expgcd  16656  nn0gcdsq  16845  pythagtriplem16  16924  4sqlem19  17057  dec5nprm  17160  dec2nprm  17161  mod2xnegi  17165  numexp2x  17172  decsplit  17176  karatsuba  17177  2exp5  17179  2exp11  17183  2exp16  17184  37prm  17215  43prm  17216  83prm  17217  139prm  17218  163prm  17219  317prm  17220  631prm  17221  1259lem1  17225  1259lem2  17226  1259lem3  17227  1259lem4  17228  1259lem5  17229  1259prm  17230  2503lem1  17231  2503lem2  17232  2503lem3  17233  2503prm  17234  4001lem1  17235  4001lem2  17236  4001lem3  17237  4001lem4  17238  4001prm  17239  funcoppc  17966  estrchom  18217  funcestrcsetclem5  18234  yonedalem3b  18369  ecqusaddd  19319  symgressbas  19508  gsum2dlem2  20097  gsumle  20271  opprrng  20485  isrhm  20619  rngqiprnglinlem2  21494  pzriprng1ALT  21708  evlsval  22301  mamudi  22624  mamudir  22625  oftpos  22673  mamutpos  22679  mdetrlin  22823  mdetrlin2  22828  mdetunilem5  22837  cpmadugsumfi  23101  cnmpt2res  23902  ussval  24484  icopnfhmeo  25170  iccpnfhmeo  25172  pcoass  25251  ovolunlem1a  25723  ioombl1lem3  25787  ioombl1lem4  25788  mbfimaopnlem  25882  itgfsum  26054  iblabslem  26055  itgsplit  26063  dveflem  26206  efhalfpi  26704  efipi  26706  sin2pi  26708  ef2pi  26710  sincosq3sgn  26733  sincosq4sgn  26734  sinq34lt0t  26742  sincos4thpi  26746  tan4thpi  26747  tan4thpiOLD  26748  sincos6thpi  26749  sincos3rdpi  26750  pigt3  26751  pige3ALT  26753  cxpcn3  26981  lawcos  27049  1cubrlem  27074  quart1lem  27088  quart1  27089  asin1  27127  atancj  27143  atanlogsublem  27148  log2cnv  27177  log2tlbnd  27178  log2ublem3  27181  log2ub  27182  birthday  27187  basellem8  27320  basellem9  27321  cht2  27404  cht3  27405  1sgm2ppw  27432  bclbnd  27512  bposlem8  27523  bposlem9  27524  lgsdi  27566  lgsquadlem1  27612  2lgsoddprmlem3c  27644  2lgsoddprmlem3d  27645  addsqnreup  27675  addsval2  28224  addsunif  28263  addsasslem1  28264  addsasslem2  28265  negsval  28286  neg0s  28287  neg1s  28288  negsid  28302  mulsval2  28372  muls01  28373  mulsproplem2  28378  mulsproplem3  28379  mulsproplem4  28380  mulsproplem5  28381  mulsproplem6  28382  mulsproplem7  28383  mulsproplem8  28384  mulsproplem12  28388  mulsproplem13  28389  mulsproplem14  28390  mulsunif  28411  addsdilem1  28412  addsdilem2  28413  mulsasslem1  28424  mulsasslem2  28425  mulsunif2  28431  precsexlem11  28478  onmulscl  28539  twocut  28684  mirauto  29031  axsegconlem9  29366  ax5seglem7  29376  vtxdginducedm1  29987  clwlkclwwlkfo  30463  eupth2eucrct  30681  ex-exp  30914  ex-fac  30915  ex-bc  30916  ex-hash  30917  ip0i  31290  ip1ilem  31291  ip2i  31293  ipdirilem  31294  ipasslem10  31304  ip2dii  31309  pythi  31315  siilem1  31316  hvsubsub4i  31524  hvsubcan2i  31529  hisubcomi  31569  normlem0  31574  normlem1  31575  normlem2  31576  normlem3  31577  normlem6  31580  normlem8  31582  normlem9  31583  bcseqi  31585  norm-ii-i  31602  norm-iii-i  31604  normpythi  31607  norm3difi  31612  normpari  31619  normpar2i  31621  polid2i  31622  polidi  31623  bcsiALT  31644  lediri  32002  h1de2i  32018  cmcmlem  32056  cmbr2i  32061  cm2j  32085  fh3i  32088  fh4i  32089  pjaddii  32140  pjsslem  32144  pjssmii  32146  pjdifnormii  32148  lnopeq0lem1  32470  lnopunilem1  32475  lnophmlem2  32482  pjsdi2i  32622  pjclem1  32660  golem1  32736  dpmul100  33327  dpmul1000  33329  dpadd2  33340  dpadd  33341  dpadd3  33342  dpmul  33343  dpmul4  33344  ccatws1f1o  33378  elrgspnlem2  33668  matdim  34110  fldext2chn  34223  constrextdg2lem  34243  constrext2chnlem  34245  iconstr  34261  cos9thpiminplylem4  34280  cos9thpiminplylem5  34281  rmulccn  34423  raddcn  34424  xrmulc1cn  34425  xrge0iifhmeo  34431  qqh0  34479  qqh1  34480  elmbfmvol2  34763  mbfmcnt  34764  eulerpartlemgvv  34872  eulerpartlemgh  34874  fib2  34898  fib3  34899  fib4  34900  fib5  34901  fib6  34902  ballotlem2  34985  ballotlemfval0  34992  ballotth  35034  hgt750lem2  35145  problem2  36230  problem4  36232  quad3  36234  ditgeq123i  36814  cbvditgvw2  36854  poimirlem30  38384  iblabsnclem  38417  dalem10  40531  cdleme0e  41075  cdleme7c  41103  cdleme20c  41169  3exp7  42904  3lexlogpow5ineq1  42905  3lexlogpow5ineq5  42911  aks4d1p1  42927  5bc2eq10  42993  aks5lem3a  43040  25or6to4  43057  sn-1ne2  43131  sqmid3api  43143  sqdeccom12  43149  sq3deccom12  43150  tan3rdpi  43212  sin2t3rdpi  43213  cos2t3rdpi  43214  rei4  43284  ipiiie0  43298  sn-0tie0  43324  mzpcompact2lem  43581  pellexlem5  43659  pellfundgt1  43709  jm2.27c  43833  areaquad  44042  resqrtvalex  44470  imsqrtvalex  44471  lhe4.4ex1a  45138  mccl  46413  dvnprodlem2  46760  itgsin0pilem1  46763  stoweidlem13  46826  wallispilem4  46881  wallispi2lem1  46884  wallispi2lem2  46885  dirkerper  46909  dirkertrigeqlem1  46911  fourierdlem30  46950  fourierdlem47  46966  fourierdlem103  47022  fourierdlem104  47023  fouriersw  47044  etransclem37  47084  sge0splitmpt  47224  sge0xaddlem2  47247  sge0xadd  47248  caragen0  47319  caragenuncllem  47325  goldpolyfactor  47730  goldrasin  47732  goldratmolem2  47736  goldratmolem3  47737  goldratval  47739  fsumsplitsndif  48254  139prmALT  48484  127prm  48487  m11nprm  48489  3exp4mod41  48504  ppivalnn4  48515  sbgoldbo  48688  2t6m3t4e0  49263  lincsum  49344  zlmodzxzequa  49411  zlmodzxzequap  49414  zlmodzxzldeplem3  49417  rrx2linest  49657  line2  49667  itsclc0yqsollem1  49677  itsclquadb  49691  itscnhlinecirc02plem2  49698  postcofval  50275  postcofcl  50276  precofval  50278  precofvalALT  50279  precofcl  50281  termcfuncval  50443