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

Theorem oveq12i 6307
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 6304 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A F C )  =  ( B F D ) )
41, 2, 3mp2an 679 1  |-  ( A F C )  =  ( B F D )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1446  (class class class)co 6295
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-rex 2745  df-rab 2748  df-v 3049  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3734  df-if 3884  df-sn 3971  df-pr 3973  df-op 3977  df-uni 4202  df-br 4406  df-iota 5549  df-fv 5593  df-ov 6298
This theorem is referenced by:  oveq123i  6309  caovdir  6508  caovdilem  6509  caovlem2  6510  cnfcom2  8212  canthwelem  9080  adderpqlem  9384  addassnq  9388  distrnq  9391  ltanq  9401  1lt2nq  9403  ltexnq  9405  halfnq  9406  mulcmpblnrlem  9499  mulcomsr  9518  distrsr  9520  m1p1sr  9521  m1m1sr  9522  mulgt0sr  9534  addcnsrec  9572  mulcnsrec  9573  axmulcom  9584  axmulass  9586  axdistr  9587  axi2m1  9588  addid1  9818  negdiiOLD  9964  3t3e9  10769  8th4div3  10840  halfpm6th  10841  numma  11089  4t3lem  11129  halfthird  11164  5recm6rec  11165  seqfeq4  12269  seqof  12277  sqdivi  12366  i4  12384  binom2i  12391  nn0opthlem1  12461  facp1  12471  fac2  12472  fac3  12473  fac4  12474  faclbnd4lem1  12485  4bc2eq6  12521  ccat2s1len  12764  ccat2s1p2  12769  cats1len  12963  cji  13234  sqrlem5  13322  fsumadd  13817  fsumsplitsnun  13828  0.999...  13949  fprodmul  14026  fproddiv  14027  fprodsplitf  14054  bpoly3  14123  fsumcube  14125  efsep  14176  ef01bndlem  14250  cos2bnd  14254  rpnnen2lem3  14281  sadeq  14458  gcdaddmlem  14504  bezout  14522  nn0gcdsq  14713  pythagtriplem16  14792  4sqlem19  14925  dec5nprm  15050  dec2nprm  15051  mod2xnegi  15055  numexp2x  15063  decsplit  15067  karatsuba  15068  2exp16  15073  37prm  15104  43prm  15105  83prm  15106  139prm  15107  163prm  15108  317prm  15109  631prm  15110  1259lem1  15114  1259lem2  15115  1259lem3  15116  1259lem4  15117  1259lem5  15118  1259prm  15119  2503lem1  15120  2503lem2  15121  2503lem3  15122  2503prm  15123  4001lem1  15124  4001lem2  15125  4001lem3  15126  4001lem4  15127  4001prm  15128  funcoppc  15792  estrchom  16024  funcestrcsetclem5  16041  yonedalem3b  16176  gsum2dlem2  17615  opprring  17871  isrhm  17961  evlsval  18754  mamudi  19440  mamudir  19441  oftpos  19489  mamutpos  19495  mdetrlin  19639  mdetrlin2  19644  mdetunilem5  19653  cpmadugsumfi  19913  cnmpt2res  20704  ussval  21286  icopnfhmeo  21983  iccpnfhmeo  21985  pcoass  22067  ovolunlem1a  22461  ioombl1lem3  22525  ioombl1lem4  22526  mbfimaopnlem  22623  iblcnlem1  22757  itgfsum  22796  iblabslem  22797  itgsplit  22805  dveflem  22943  efhalfpi  23438  efipi  23440  sin2pi  23442  ef2pi  23444  sincosq3sgn  23467  sincosq4sgn  23468  sinq34lt0t  23476  sincos4thpi  23480  tan4thpi  23481  sincos6thpi  23482  sincos3rdpi  23483  pige3  23484  cxpcn3  23700  lawcos  23757  1cubrlem  23779  quart1lem  23793  quart1  23794  asin1  23832  atancj  23848  atanlogsublem  23853  log2cnv  23882  log2tlbnd  23883  log2ublem3  23886  log2ub  23887  birthday  23892  basellem8  24026  basellem9  24027  cht2  24111  cht3  24112  1sgm2ppw  24140  bclbnd  24220  bposlem8  24231  bposlem9  24232  lgsdi  24272  lgsquadlem1  24294  mirauto  24741  axsegconlem9  24967  ax5seglem7  24977  clwlkfoclwwlk  25585  vdgr0  25640  vdegp1bi  25725  ip0i  26478  ip1ilem  26479  ip2i  26481  ipdirilem  26482  ipasslem10  26492  ip2dii  26497  pythi  26503  siilem1  26504  hvsubsub4i  26724  hvsubcan2i  26729  hisubcomi  26769  normlem0  26774  normlem1  26775  normlem2  26776  normlem3  26777  normlem6  26780  normlem8  26782  normlem9  26783  bcseqi  26785  norm-ii-i  26802  norm-iii-i  26804  normpythi  26807  norm3difi  26812  normpari  26819  normpar2i  26821  polid2i  26822  polidi  26823  bcsiALT  26844  lediri  27202  h1de2i  27218  cmcmlem  27256  cmbr2i  27261  cm2j  27285  fh3i  27288  fh4i  27289  pjaddii  27340  pjsslem  27344  pjssmii  27346  pjdifnormii  27348  lnopeq0lem1  27670  lnopunilem1  27675  lnophmlem2  27682  pjsdi2i  27822  pjclem1  27860  golem1  27936  gsumle  28554  rmulccn  28746  raddcn  28747  xrmulc1cn  28748  xrge0iifhmeo  28754  qqh0  28800  qqh1  28801  elmbfmvol2  29101  mbfmcnt  29102  eulerpartlemgvv  29221  eulerpartlemgh  29223  fib2  29247  fib3  29248  fib4  29249  fib5  29250  fib6  29251  ballotlem2  29333  ballotlemfval0  29340  ballotth  29382  ballotthOLD  29420  ofs2  29445  problem2  30310  problem4  30312  quad3  30314  pigt3  31950  poimirlem30  31982  iblabsnclem  32017  dalem10  33250  cdleme0e  33795  cdleme7c  33823  cdleme20c  33890  mzpcompact2lem  35605  pellexlem5  35689  pellfundgt1  35743  jm2.27c  35874  areaquad  36113  lhe4.4ex1a  36689  fsumsplitf  37656  mccl  37688  dvnprodlem2  37832  itgsin0pilem1  37836  stoweidlem13  37883  wallispilem4  37940  wallispi2lem1  37943  wallispi2lem2  37944  dirkerper  37968  dirkertrigeqlem1  37970  fourierdlem30  38009  fourierdlem47  38027  fourierdlem103  38083  fourierdlem104  38084  fouriersw  38105  etransclem37  38146  sge0splitmpt  38263  sge0xaddlem2  38286  sge0xadd  38287  caragen0  38337  caragenuncllem  38343  3exp4mod41  38926  fsumsplitsndif  39102  2t6m3t4e0  40233  lincsum  40326  zlmodzxzequa  40393  zlmodzxzequap  40396  zlmodzxzldeplem3  40399
  Copyright terms: Public domain W3C validator