Theorem oveq12i 7033

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

Syntax hints:   = wceq 1522  (class class class)co 7021

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-rex 3111  df-rab 3114  df-v 3439  df-dif 3866  df-un 3868  df-in 3870  df-ss 3878  df-nul 4216  df-if 4386  df-sn 4477  df-pr 4479  df-op 4483  df-uni 4750  df-br 4967  df-iota 6194  df-fv 6238  df-ov 7024

This theorem is referenced by:  oveq123i  7035  caovdir  7243  caovdilem  7244  caovlem2  7245  cnfcom2  9016  canthwelem  9923  adderpqlem  10227  addassnq  10231  distrnq  10234  ltanq  10244  1lt2nq  10246  ltexnq  10248  halfnq  10249  mulcmpblnrlem  10343  mulcomsr  10362  distrsr  10364  m1p1sr  10365  m1m1sr  10366  mulgt0sr  10378  addcnsrec  10416  mulcnsrec  10417  axmulcom  10428  axmulass  10430  axdistr  10431  axi2m1  10432  addid1  10672  3t3e9  11657  8th4div3  11710  halfpm6th  11711  numma  11996  decmul10add  12022  4t3lem  12050  9t11e99  12083  halfthird  12096  5recm6rec  12097  fz0to3un2pr  12864  seqfeq4  13274  seqof  13282  sqdivi  13403  sq4e2t8  13417  i4  13422  binom2i  13429  nn0opthlem1  13483  facp1  13493  fac2  13494  fac3  13495  fac4  13496  faclbnd4lem1  13508  4bc2eq6  13544  ccat2s1len  13826  ccat2s1p2  13833  cats1len  14063  cats2cat  14065  ofs2  14170  cji  14357  sqrlem5  14445  fsumadd  14934  fsumsplitf  14936  fsumsplitsnun  14948  0.999...  15075  fprodmul  15152  fproddiv  15153  fprodsplitf  15180  bpoly3  15250  fsumcube  15252  efsep  15301  ef01bndlem  15375  cos2bnd  15379  rpnnen2lem3  15407  3dvds2dec  15520  flodddiv4  15602  sadeq  15659  gcdaddmlem  15710  bezout  15725  nn0gcdsq  15926  pythagtriplem16  16001  4sqlem19  16133  dec5nprm  16236  dec2nprm  16237  mod2xnegi  16241  numexp2x  16249  decsplit  16253  karatsuba  16254  2exp16  16258  37prm  16288  43prm  16289  83prm  16290  139prm  16291  163prm  16292  317prm  16293  631prm  16294  1259lem1  16298  1259lem2  16299  1259lem3  16300  1259lem4  16301  1259lem5  16302  1259prm  16303  2503lem1  16304  2503lem2  16305  2503lem3  16306  2503prm  16307  4001lem1  16308  4001lem2  16309  4001lem3  16310  4001lem4  16311  4001prm  16312  funcoppc  16979  estrchom  17211  funcestrcsetclem5  17228  yonedalem3b  17363  gsum2dlem2  18816  opprring  19076  isrhm  19168  evlsval  19991  mamudi  20701  mamudir  20702  oftpos  20750  mamutpos  20756  mdetrlin  20900  mdetrlin2  20905  mdetunilem5  20914  cpmadugsumfi  21174  cnmpt2res  21974  ussval  22556  icopnfhmeo  23235  iccpnfhmeo  23237  pcoass  23316  ovolunlem1a  23785  ioombl1lem3  23849  ioombl1lem4  23850  mbfimaopnlem  23944  itgfsum  24115  iblabslem  24116  itgsplit  24124  dveflem  24264  efhalfpi  24745  efipi  24747  sin2pi  24749  ef2pi  24751  sincosq3sgn  24774  sincosq4sgn  24775  sinq34lt0t  24783  sincos4thpi  24787  tan4thpi  24788  sincos6thpi  24789  sincos3rdpi  24790  pigt3  24791  pige3ALT  24793  cxpcn3  25015  lawcos  25080  1cubrlem  25105  quart1lem  25119  quart1  25120  asin1  25158  atancj  25174  atanlogsublem  25179  log2cnv  25209  log2tlbnd  25210  log2ublem3  25213  log2ub  25214  birthday  25219  basellem8  25352  basellem9  25353  cht2  25436  cht3  25437  1sgm2ppw  25463  bclbnd  25543  bposlem8  25554  bposlem9  25555  lgsdi  25597  lgsquadlem1  25643  2lgsoddprmlem3c  25675  2lgsoddprmlem3d  25676  addsqnreup  25706  mirauto  26157  axsegconlem9  26399  ax5seglem7  26409  vtxdginducedm1  27013  clwlkclwwlkfo  27479  eupth2eucrct  27689  ex-exp  27926  ex-fac  27927  ex-bc  27928  ex-hash  27929  ip0i  28298  ip1ilem  28299  ip2i  28301  ipdirilem  28302  ipasslem10  28312  ip2dii  28317  pythi  28323  siilem1  28324  hvsubsub4i  28532  hvsubcan2i  28537  hisubcomi  28577  normlem0  28582  normlem1  28583  normlem2  28584  normlem3  28585  normlem6  28588  normlem8  28590  normlem9  28591  bcseqi  28593  norm-ii-i  28610  norm-iii-i  28612  normpythi  28615  norm3difi  28620  normpari  28627  normpar2i  28629  polid2i  28630  polidi  28631  bcsiALT  28652  lediri  29010  h1de2i  29026  cmcmlem  29064  cmbr2i  29069  cm2j  29093  fh3i  29096  fh4i  29097  pjaddii  29148  pjsslem  29152  pjssmii  29154  pjdifnormii  29156  lnopeq0lem1  29478  lnopunilem1  29483  lnophmlem2  29490  pjsdi2i  29630  pjclem1  29668  golem1  29744  dpmul100  30262  dpmul1000  30264  dpadd2  30275  dpadd  30276  dpadd3  30277  dpmul  30278  dpmul4  30279  gsumle  30499  matdim  30622  rmulccn  30793  raddcn  30794  xrmulc1cn  30795  xrge0iifhmeo  30801  qqh0  30847  qqh1  30848  elmbfmvol2  31147  mbfmcnt  31148  eulerpartlemgvv  31256  eulerpartlemgh  31258  fib2  31282  fib3  31283  fib4  31284  fib5  31285  fib6  31286  ballotlem2  31368  ballotlemfval0  31375  ballotth  31417  hgt750lem2  31545  problem2  32523  problem4  32525  quad3  32527  poimirlem30  34478  iblabsnclem  34511  dalem10  36365  cdleme0e  36909  cdleme7c  36937  cdleme20c  37003  sqmid3api  38716  sqdeccom12  38722  sq3deccom12  38723  nn0expgcd  38731  mzpcompact2lem  38858  pellexlem5  38940  pellfundgt1  38990  jm2.27c  39114  areaquad  39333  lhe4.4ex1a  40224  mccl  41446  dvnprodlem2  41799  itgsin0pilem1  41802  stoweidlem13  41866  wallispilem4  41921  wallispi2lem1  41924  wallispi2lem2  41925  dirkerper  41949  dirkertrigeqlem1  41951  fourierdlem30  41990  fourierdlem47  42006  fourierdlem103  42062  fourierdlem104  42063  fouriersw  42084  etransclem37  42124  sge0splitmpt  42261  sge0xaddlem2  42284  sge0xadd  42285  caragen0  42356  caragenuncllem  42362  fsumsplitsndif  43075  2exp5  43263  139prmALT  43267  127prm  43271  2exp11  43273  m11nprm  43274  3exp4mod41  43289  sbgoldbo  43460  2t6m3t4e0  43900  lincsum  43990  zlmodzxzequa  44057  zlmodzxzequap  44060  zlmodzxzldeplem3  44063  rrx2linest  44236  line2  44246  itsclc0yqsollem1  44256  itsclquadb  44270  itscnhlinecirc02plem2  44277