Theorem oveq12i 7442

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

Syntax hints:   = wceq 1536  (class class class)co 7430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433

This theorem is referenced by:  oveq123i  7444  caovdir  7666  caovdilem  7667  caovlem2  7668  cnfcom2  9739  canthwelem  10687  adderpqlem  10991  addassnq  10995  distrnq  10998  ltanq  11008  1lt2nq  11010  ltexnq  11012  halfnq  11013  mulcmpblnrlem  11107  mulcomsr  11126  distrsr  11128  m1p1sr  11129  m1m1sr  11130  mulgt0sr  11142  addcnsrec  11180  mulcnsrec  11181  axmulcom  11192  axmulass  11194  axdistr  11195  axi2m1  11196  addrid  11438  3t3e9  12430  8th4div3  12483  halfpm6th  12484  numma  12774  decmul10add  12799  4t3lem  12827  9t11e99  12860  halfthird  12873  5recm6rec  12874  fz0to3un2pr  13665  seqfeq4  14088  seqof  14096  sqdivi  14220  sq4e2t8  14234  i4  14239  binom2i  14247  nn0opthlem1  14303  facp1  14313  fac2  14314  fac3  14315  fac4  14316  faclbnd4lem1  14328  4bc2eq6  14364  ccat2s1len  14657  ccat2s1p2  14664  cats1len  14895  cats2cat  14897  ofs2  15006  cji  15194  01sqrexlem5  15281  fsumadd  15772  fsumsplitf  15774  fsumsplitsnun  15787  0.999...  15913  fprodmul  15992  fproddiv  15993  fprodsplitf  16020  bpoly3  16090  fsumcube  16092  efsep  16142  ef01bndlem  16216  cos2bnd  16220  rpnnen2lem3  16248  3dvds2dec  16366  flodddiv4  16448  sadeq  16505  gcdaddmlem  16557  bezout  16576  nn0expgcd  16597  nn0gcdsq  16785  pythagtriplem16  16863  4sqlem19  16996  dec5nprm  17099  dec2nprm  17100  mod2xnegi  17104  numexp2x  17112  decsplit  17116  karatsuba  17117  2exp5  17119  2exp11  17123  2exp16  17124  37prm  17154  43prm  17155  83prm  17156  139prm  17157  163prm  17158  317prm  17159  631prm  17160  1259lem1  17164  1259lem2  17165  1259lem3  17166  1259lem4  17167  1259lem5  17168  1259prm  17169  2503lem1  17170  2503lem2  17171  2503lem3  17172  2503prm  17173  4001lem1  17174  4001lem2  17175  4001lem3  17176  4001lem4  17177  4001prm  17178  funcoppc  17925  estrchom  18181  funcestrcsetclem5  18199  yonedalem3b  18335  ecqusaddd  19222  symgressbas  19413  gsum2dlem2  20003  opprrng  20361  isrhm  20494  rngqiprnglinlem2  21319  pzriprng1ALT  21524  evlsval  22127  mamudi  22422  mamudir  22423  oftpos  22473  mamutpos  22479  mdetrlin  22623  mdetrlin2  22628  mdetunilem5  22637  cpmadugsumfi  22898  cnmpt2res  23700  ussval  24283  icopnfhmeo  24987  iccpnfhmeo  24989  pcoass  25070  ovolunlem1a  25544  ioombl1lem3  25608  ioombl1lem4  25609  mbfimaopnlem  25703  itgfsum  25876  iblabslem  25877  itgsplit  25885  dveflem  26031  efhalfpi  26527  efipi  26529  sin2pi  26531  ef2pi  26533  sincosq3sgn  26556  sincosq4sgn  26557  sinq34lt0t  26565  sincos4thpi  26569  tan4thpi  26570  tan4thpiOLD  26571  sincos6thpi  26572  sincos3rdpi  26573  pigt3  26574  pige3ALT  26576  cxpcn3  26805  lawcos  26873  1cubrlem  26898  quart1lem  26912  quart1  26913  asin1  26951  atancj  26967  atanlogsublem  26972  log2cnv  27001  log2tlbnd  27002  log2ublem3  27005  log2ub  27006  birthday  27011  basellem8  27145  basellem9  27146  cht2  27229  cht3  27230  1sgm2ppw  27258  bclbnd  27338  bposlem8  27349  bposlem9  27350  lgsdi  27392  lgsquadlem1  27438  2lgsoddprmlem3c  27470  2lgsoddprmlem3d  27471  addsqnreup  27501  addsval2  28010  addsunif  28049  addsasslem1  28050  addsasslem2  28051  negsval  28071  negs0s  28072  negs1s  28073  negsid  28087  mulsval2  28151  muls01  28152  mulsproplem2  28157  mulsproplem3  28158  mulsproplem4  28159  mulsproplem5  28160  mulsproplem6  28161  mulsproplem7  28162  mulsproplem8  28163  mulsproplem12  28167  mulsproplem13  28168  mulsproplem14  28169  mulsunif  28190  addsdilem1  28191  addsdilem2  28192  mulsasslem1  28203  mulsasslem2  28204  mulsunif2  28210  precsexlem11  28255  onmulscl  28301  1p1e2s  28414  nohalf  28421  0reno  28443  mirauto  28706  axsegconlem9  28954  ax5seglem7  28964  vtxdginducedm1  29575  clwlkclwwlkfo  30037  eupth2eucrct  30245  ex-exp  30478  ex-fac  30479  ex-bc  30480  ex-hash  30481  ip0i  30853  ip1ilem  30854  ip2i  30856  ipdirilem  30857  ipasslem10  30867  ip2dii  30872  pythi  30878  siilem1  30879  hvsubsub4i  31087  hvsubcan2i  31092  hisubcomi  31132  normlem0  31137  normlem1  31138  normlem2  31139  normlem3  31140  normlem6  31143  normlem8  31145  normlem9  31146  bcseqi  31148  norm-ii-i  31165  norm-iii-i  31167  normpythi  31170  norm3difi  31175  normpari  31182  normpar2i  31184  polid2i  31185  polidi  31186  bcsiALT  31207  lediri  31565  h1de2i  31581  cmcmlem  31619  cmbr2i  31624  cm2j  31648  fh3i  31651  fh4i  31652  pjaddii  31703  pjsslem  31707  pjssmii  31709  pjdifnormii  31711  lnopeq0lem1  32033  lnopunilem1  32038  lnophmlem2  32045  pjsdi2i  32185  pjclem1  32223  golem1  32299  dpmul100  32863  dpmul1000  32865  dpadd2  32876  dpadd  32877  dpadd3  32878  dpmul  32879  dpmul4  32880  ccatws1f1o  32920  gsumle  33083  elrgspnlem2  33232  matdim  33642  rmulccn  33888  raddcn  33889  xrmulc1cn  33890  xrge0iifhmeo  33896  qqh0  33946  qqh1  33947  elmbfmvol2  34248  mbfmcnt  34249  eulerpartlemgvv  34357  eulerpartlemgh  34359  fib2  34383  fib3  34384  fib4  34385  fib5  34386  fib6  34387  ballotlem2  34469  ballotlemfval0  34476  ballotth  34518  hgt750lem2  34645  problem2  35650  problem4  35652  quad3  35654  ditgeq123i  36190  cbvditgvw2  36231  poimirlem30  37636  iblabsnclem  37669  dalem10  39655  cdleme0e  40199  cdleme7c  40227  cdleme20c  40293  3exp7  42034  3lexlogpow5ineq1  42035  3lexlogpow5ineq5  42041  aks4d1p1  42057  5bc2eq10  42123  aks5lem3a  42170  sn-1ne2  42278  sqmid3api  42296  sqdeccom12  42302  sq3deccom12  42303  tan3rdpi  42364  rei4  42429  ipiiie0  42443  sn-0tie0  42445  mzpcompact2lem  42738  pellexlem5  42820  pellfundgt1  42870  jm2.27c  42995  areaquad  43204  resqrtvalex  43634  imsqrtvalex  43635  lhe4.4ex1a  44324  mccl  45553  dvnprodlem2  45902  itgsin0pilem1  45905  stoweidlem13  45968  wallispilem4  46023  wallispi2lem1  46026  wallispi2lem2  46027  dirkerper  46051  dirkertrigeqlem1  46053  fourierdlem30  46092  fourierdlem47  46108  fourierdlem103  46164  fourierdlem104  46165  fouriersw  46186  etransclem37  46226  sge0splitmpt  46366  sge0xaddlem2  46389  sge0xadd  46390  caragen0  46461  caragenuncllem  46467  fsumsplitsndif  47297  139prmALT  47520  127prm  47523  m11nprm  47525  3exp4mod41  47540  sbgoldbo  47711  2t6m3t4e0  48192  lincsum  48274  zlmodzxzequa  48341  zlmodzxzequap  48344  zlmodzxzldeplem3  48347  rrx2linest  48591  line2  48601  itsclc0yqsollem1  48611  itsclquadb  48625  itscnhlinecirc02plem2  48632