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

Theorem oveq12i 6098
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 6095 . 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 1369  (class class class)co 6086
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rex 2716  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-iota 5376  df-fv 5421  df-ov 6089
This theorem is referenced by:  oveq123i  6100  caovdir  6292  caovdilem  6293  caovlem2  6294  cnfcom2  7927  cnfcom2OLD  7935  canthwelem  8809  adderpqlem  9115  addassnq  9119  distrnq  9122  ltanq  9132  1lt2nq  9134  ltexnq  9136  halfnq  9137  mulcmpblnrlem  9232  mulcomsr  9248  distrsr  9250  m1p1sr  9251  m1m1sr  9252  mulgt0sr  9264  addcnsrec  9302  mulcnsrec  9303  axmulcom  9314  axmulass  9316  axdistr  9317  axi2m1  9318  addid1  9541  negdii  9684  3t3e9  10466  8th4div3  10537  halfpm6th  10538  numma  10778  4t3lem  10818  seqfeq4  11847  seqof  11855  sqdivi  11942  i4  11960  binom2i  11967  binom2aiOLD  11968  nn0opthlem1  12038  facp1  12048  fac2  12049  fac3  12050  fac4  12051  faclbnd4lem1  12061  cats1len  12479  cji  12640  sqrlem5  12728  fsumadd  13207  0.999...  13333  efsep  13386  ef01bndlem  13460  cos2bnd  13464  rpnnen2lem3  13491  sadeq  13660  gcdaddmlem  13704  bezout  13718  nn0gcdsq  13822  pythagtriplem16  13889  4sqlem19  14016  dec5nprm  14087  dec2nprm  14088  mod2xnegi  14092  numexp2x  14100  decsplit  14104  karatsuba  14105  2exp16  14109  37prm  14140  43prm  14141  83prm  14142  139prm  14143  163prm  14144  317prm  14145  631prm  14146  1259lem1  14147  1259lem2  14148  1259lem3  14149  1259lem4  14150  1259lem5  14151  1259prm  14152  2503lem1  14153  2503lem2  14154  2503lem3  14155  2503prm  14156  4001lem1  14157  4001lem2  14158  4001lem3  14159  4001lem4  14160  4001prm  14161  funcoppc  14777  yonedalem3b  15081  gsum2dlem2  16450  gsum2dOLD  16452  opprrng  16711  isrhm  16799  evlsval  17580  mamudi  18282  mamudir  18283  oftpos  18308  mamutpos  18318  mdetrlin  18384  mdetrlin2  18388  mdetunilem5  18397  cnmpt2res  19225  ussval  19809  icopnfhmeo  20490  iccpnfhmeo  20492  pcoass  20571  ovolunlem1a  20954  ioombl1lem3  21016  ioombl1lem4  21017  mbfimaopnlem  21108  iblcnlem1  21240  itgfsum  21279  iblabslem  21280  itgsplit  21288  dveflem  21426  efhalfpi  21908  efipi  21910  sin2pi  21912  ef2pi  21914  sincosq3sgn  21937  sincosq4sgn  21938  sinq34lt0t  21946  sincos4thpi  21950  tan4thpi  21951  sincos6thpi  21952  sincos3rdpi  21953  pige3  21954  cxpcn3  22161  lawcos  22187  1cubrlem  22211  quart1lem  22225  quart1  22226  asin1  22264  atancj  22280  atanlogsublem  22285  log2cnv  22314  log2tlbnd  22315  log2ublem3  22318  log2ub  22319  birthday  22323  basellem8  22400  basellem9  22401  cht2  22485  cht3  22486  1sgm2ppw  22514  bclbnd  22594  bposlem8  22605  bposlem9  22606  lgsdi  22646  lgsquadlem1  22668  mirauto  23043  axsegconlem9  23122  ax5seglem7  23132  vdgr0  23521  vdegp1bi  23557  ip0i  24176  ip1ilem  24177  ip2i  24179  ipdirilem  24180  ipasslem10  24190  ip2dii  24195  pythi  24201  siilem1  24202  hvsubsub4i  24412  hvsubcan2i  24417  hisubcomi  24457  normlem0  24462  normlem1  24463  normlem2  24464  normlem3  24465  normlem6  24468  normlem8  24470  normlem9  24471  bcseqi  24473  norm-ii-i  24490  norm-iii-i  24492  normpythi  24495  norm3difi  24500  normpari  24507  normpar2i  24509  polid2i  24510  polidi  24511  bcsiALT  24532  lediri  24891  h1de2i  24907  cmcmlem  24945  cmbr2i  24950  cm2j  24974  fh3i  24977  fh4i  24978  pjaddii  25029  pjsslem  25033  pjssmii  25035  pjdifnormii  25037  lnopeq0lem1  25360  lnopunilem1  25365  lnophmlem2  25372  pjsdi2i  25512  pjclem1  25550  golem1  25626  gsumle  26197  gsummptun  26199  rmulccn  26310  raddcn  26311  xrmulc1cn  26312  xrge0iifhmeo  26318  qqh0  26365  qqh1  26366  elmbfmvol2  26634  mbfmcnt  26635  eulerpartlemgvv  26711  eulerpartlemgh  26713  fib2  26737  fib3  26738  fib4  26739  fib5  26740  fib6  26741  ballotlem2  26823  ballotlemfval0  26830  ballotth  26872  ofs2  26897  signstfveq0  26930  problem2  27251  problem4  27253  4bc2eq6  27342  halfthird  27343  5recm6rec  27344  fprodmul  27422  fproddiv  27423  bpoly3  28152  fsumcube  28154  iblabsnclem  28408  mzpcompact2lem  29041  pellexlem5  29127  pellfundgt1  29177  jm2.27c  29309  areaquad  29545  lhe4.4ex1a  29556  itgsin0pilem1  29743  stoweidlem13  29761  wallispilem4  29816  wallispi2lem1  29819  wallispi2lem2  29820  fsumsplitsndif  30191  fsumsplitsnun  30195  ccat2s1len  30217  ccat2s1p2  30219  clwlkfoclwwlk  30471  2t6m3t4e0  30692  lincsum  30852  zlmodzxzequa  30927  zlmodzxzequap  30930  zlmodzxzldeplem3  30933  dalem10  33157  cdleme0e  33701  cdleme7c  33729  cdleme20c  33795
  Copyright terms: Public domain W3C validator