MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  oveq12i Structured version   Unicode version

Theorem oveq12i 6211
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  |-  A  =  B
oveq12i.2  |-  C  =  D
Assertion
Ref Expression
oveq12i  |-  ( A F C )  =  ( B F D )

Proof of Theorem oveq12i
StepHypRef Expression
1 oveq1i.1 . 2  |-  A  =  B
2 oveq12i.2 . 2  |-  C  =  D
3 oveq12 6208 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A F C )  =  ( B F D ) )
41, 2, 3mp2an 672 1  |-  ( A F C )  =  ( B F D )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1370  (class class class)co 6199
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rex 2804  df-rab 2807  df-v 3078  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-sn 3985  df-pr 3987  df-op 3991  df-uni 4199  df-br 4400  df-iota 5488  df-fv 5533  df-ov 6202
This theorem is referenced by:  oveq123i  6213  caovdir  6406  caovdilem  6407  caovlem2  6408  cnfcom2  8045  cnfcom2OLD  8053  canthwelem  8927  adderpqlem  9233  addassnq  9237  distrnq  9240  ltanq  9250  1lt2nq  9252  ltexnq  9254  halfnq  9255  mulcmpblnrlem  9350  mulcomsr  9366  distrsr  9368  m1p1sr  9369  m1m1sr  9370  mulgt0sr  9382  addcnsrec  9420  mulcnsrec  9421  axmulcom  9432  axmulass  9434  axdistr  9435  axi2m1  9436  addid1  9659  negdii  9802  3t3e9  10584  8th4div3  10655  halfpm6th  10656  numma  10896  4t3lem  10936  seqfeq4  11971  seqof  11979  sqdivi  12066  i4  12084  binom2i  12091  binom2aiOLD  12092  nn0opthlem1  12162  facp1  12172  fac2  12173  fac3  12174  fac4  12175  faclbnd4lem1  12185  cats1len  12604  cji  12765  sqrlem5  12853  fsumadd  13332  0.999...  13458  efsep  13511  ef01bndlem  13585  cos2bnd  13589  rpnnen2lem3  13616  sadeq  13785  gcdaddmlem  13829  bezout  13843  nn0gcdsq  13947  pythagtriplem16  14014  4sqlem19  14141  dec5nprm  14212  dec2nprm  14213  mod2xnegi  14217  numexp2x  14225  decsplit  14229  karatsuba  14230  2exp16  14234  37prm  14265  43prm  14266  83prm  14267  139prm  14268  163prm  14269  317prm  14270  631prm  14271  1259lem1  14272  1259lem2  14273  1259lem3  14274  1259lem4  14275  1259lem5  14276  1259prm  14277  2503lem1  14278  2503lem2  14279  2503lem3  14280  2503prm  14281  4001lem1  14282  4001lem2  14283  4001lem3  14284  4001lem4  14285  4001prm  14286  funcoppc  14903  yonedalem3b  15207  gsum2dlem2  16583  gsum2dOLD  16585  opprrng  16845  isrhm  16933  evlsval  17728  mamudi  18431  mamudir  18432  oftpos  18459  mamutpos  18469  mdetrlin  18539  mdetrlin2  18544  mdetunilem5  18553  cnmpt2res  19381  ussval  19965  icopnfhmeo  20646  iccpnfhmeo  20648  pcoass  20727  ovolunlem1a  21110  ioombl1lem3  21173  ioombl1lem4  21174  mbfimaopnlem  21265  iblcnlem1  21397  itgfsum  21436  iblabslem  21437  itgsplit  21445  dveflem  21583  efhalfpi  22065  efipi  22067  sin2pi  22069  ef2pi  22071  sincosq3sgn  22094  sincosq4sgn  22095  sinq34lt0t  22103  sincos4thpi  22107  tan4thpi  22108  sincos6thpi  22109  sincos3rdpi  22110  pige3  22111  cxpcn3  22318  lawcos  22344  1cubrlem  22368  quart1lem  22382  quart1  22383  asin1  22421  atancj  22437  atanlogsublem  22442  log2cnv  22471  log2tlbnd  22472  log2ublem3  22475  log2ub  22476  birthday  22480  basellem8  22557  basellem9  22558  cht2  22642  cht3  22643  1sgm2ppw  22671  bclbnd  22751  bposlem8  22762  bposlem9  22763  lgsdi  22803  lgsquadlem1  22825  mirauto  23220  axsegconlem9  23322  ax5seglem7  23332  vdgr0  23721  vdegp1bi  23757  ip0i  24376  ip1ilem  24377  ip2i  24379  ipdirilem  24380  ipasslem10  24390  ip2dii  24395  pythi  24401  siilem1  24402  hvsubsub4i  24612  hvsubcan2i  24617  hisubcomi  24657  normlem0  24662  normlem1  24663  normlem2  24664  normlem3  24665  normlem6  24668  normlem8  24670  normlem9  24671  bcseqi  24673  norm-ii-i  24690  norm-iii-i  24692  normpythi  24695  norm3difi  24700  normpari  24707  normpar2i  24709  polid2i  24710  polidi  24711  bcsiALT  24732  lediri  25091  h1de2i  25107  cmcmlem  25145  cmbr2i  25150  cm2j  25174  fh3i  25177  fh4i  25178  pjaddii  25229  pjsslem  25233  pjssmii  25235  pjdifnormii  25237  lnopeq0lem1  25560  lnopunilem1  25565  lnophmlem2  25572  pjsdi2i  25712  pjclem1  25750  golem1  25826  gsumle  26390  gsummptun  26392  rmulccn  26502  raddcn  26503  xrmulc1cn  26504  xrge0iifhmeo  26510  qqh0  26557  qqh1  26558  elmbfmvol2  26825  mbfmcnt  26826  eulerpartlemgvv  26902  eulerpartlemgh  26904  fib2  26928  fib3  26929  fib4  26930  fib5  26931  fib6  26932  ballotlem2  27014  ballotlemfval0  27021  ballotth  27063  ofs2  27088  signstfveq0  27121  problem2  27442  problem4  27444  quad3  27446  4bc2eq6  27534  halfthird  27535  5recm6rec  27536  fprodmul  27614  fproddiv  27615  bpoly3  28344  fsumcube  28346  iblabsnclem  28602  mzpcompact2lem  29235  pellexlem5  29321  pellfundgt1  29371  jm2.27c  29503  areaquad  29739  lhe4.4ex1a  29750  itgsin0pilem1  29937  stoweidlem13  29955  wallispilem4  30010  wallispi2lem1  30013  wallispi2lem2  30014  fsumsplitsndif  30385  fsumsplitsnun  30389  ccat2s1len  30411  ccat2s1p2  30413  clwlkfoclwwlk  30665  2t6m3t4e0  30887  lincsum  31081  zlmodzxzequa  31156  zlmodzxzequap  31159  zlmodzxzldeplem3  31162  cpmadugsumfi  31348  dalem10  33640  cdleme0e  34184  cdleme7c  34212  cdleme20c  34278
  Copyright terms: Public domain W3C validator