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

Theorem oveq12i 6052
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 6049 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A F C )  =  ( B F D ) )
41, 2, 3mp2an 654 1  |-  ( A F C )  =  ( B F D )
Colors of variables: wff set class
Syntax hints:    = wceq 1649  (class class class)co 6040
This theorem is referenced by:  oveq123i  6054  caovdir  6240  caovdilem  6241  caovlem2  6242  cnfcom2  7615  canthwelem  8481  adderpqlem  8787  addassnq  8791  distrnq  8794  ltanq  8804  1lt2nq  8806  ltexnq  8808  halfnq  8809  mulcmpblnrlem  8904  mulcomsr  8920  distrsr  8922  m1p1sr  8923  m1m1sr  8924  mulgt0sr  8936  addcnsrec  8974  mulcnsrec  8975  axmulcom  8986  axmulass  8988  axdistr  8989  axi2m1  8990  addid1  9202  negdii  9340  3t3e9  10085  8th4div3  10147  halfpm6th  10148  numma  10369  4t3lem  10409  seqfeq4  11327  seqof  11335  sqdivi  11421  i4  11438  binom2i  11445  binom2aiOLD  11446  nn0opthlem1  11516  facp1  11526  fac2  11527  fac3  11528  fac4  11529  faclbnd4lem1  11539  cats1len  11779  cji  11919  sqrlem5  12007  fsumadd  12487  0.999...  12613  efsep  12666  ef01bndlem  12740  cos2bnd  12744  rpnnen2lem3  12771  sadeq  12939  gcdaddmlem  12983  bezout  12997  nn0gcdsq  13099  pythagtriplem16  13159  4sqlem19  13286  dec5nprm  13357  dec2nprm  13358  mod2xnegi  13362  numexp2x  13370  decsplit  13374  karatsuba  13375  2exp16  13379  37prm  13398  43prm  13399  83prm  13400  139prm  13401  163prm  13402  317prm  13403  631prm  13404  1259lem1  13405  1259lem2  13406  1259lem3  13407  1259lem4  13408  1259lem5  13409  1259prm  13410  2503lem1  13411  2503lem2  13412  2503lem3  13413  2503prm  13414  4001lem1  13415  4001lem2  13416  4001lem3  13417  4001lem4  13418  4001prm  13419  funcoppc  14027  yonedalem3b  14331  gsum2d  15501  opprrng  15691  isrhm  15779  cnmpt2res  17662  ussval  18242  icopnfhmeo  18921  iccpnfhmeo  18923  pcoass  19002  ovolunlem1a  19345  ioombl1lem3  19407  ioombl1lem4  19408  mbfimaopnlem  19500  iblcnlem1  19632  itgfsum  19671  iblabslem  19672  itgsplit  19680  dveflem  19816  evlsval  19893  efhalfpi  20332  efipi  20334  sin2pi  20336  ef2pi  20338  sincosq3sgn  20361  sincosq4sgn  20362  sinq34lt0t  20370  sincos4thpi  20374  tan4thpi  20375  sincos6thpi  20376  sincos3rdpi  20377  pige3  20378  cxpcn3  20585  lawcos  20611  1cubrlem  20634  quart1lem  20648  quart1  20649  asin1  20687  atancj  20703  atanlogsublem  20708  log2cnv  20737  log2tlbnd  20738  log2ublem3  20741  log2ub  20742  birthday  20746  basellem8  20823  basellem9  20824  cht2  20908  cht3  20909  1sgm2ppw  20937  bclbnd  21017  bposlem8  21028  bposlem9  21029  lgsdi  21069  lgsquadlem1  21091  vdgr0  21624  vdegp1bi  21660  ip0i  22279  ip1ilem  22280  ip2i  22282  ipdirilem  22283  ipasslem10  22293  ip2dii  22298  pythi  22304  siilem1  22305  hvsubsub4i  22514  hvsubcan2i  22519  hisubcomi  22559  normlem0  22564  normlem1  22565  normlem2  22566  normlem3  22567  normlem6  22570  normlem8  22572  normlem9  22573  bcseqi  22575  norm-ii-i  22592  norm-iii-i  22594  normpythi  22597  norm3difi  22602  normpari  22609  normpar2i  22611  polid2i  22612  polidi  22613  bcsiALT  22634  lediri  22992  h1de2i  23008  cmcmlem  23046  cmbr2i  23051  cm2j  23075  fh3i  23078  fh4i  23079  pjaddii  23130  pjsslem  23134  pjssmii  23136  pjdifnormii  23138  lnopeq0lem1  23461  lnopunilem1  23466  lnophmlem2  23473  pjsdi2i  23613  pjclem1  23651  golem1  23727  rmulccn  24267  raddcn  24268  xrmulc1cn  24269  xrge0iifhmeo  24275  qqh0  24321  qqh1  24322  elmbfmvol2  24570  mbfmcnt  24571  ballotlem2  24699  ballotlemfval0  24706  ballotth  24748  4bc2eq6  25157  halfthird  25158  5recm6rec  25159  fprodmul  25237  fproddiv  25238  axsegconlem9  25768  ax5seglem7  25778  bpoly3  26008  fsumcube  26010  iblabsnclem  26167  mzpcompact2lem  26698  pellexlem5  26786  pellfundgt1  26836  jm2.27c  26968  mamudi  27329  mamudir  27330  lhe4.4ex1a  27414  itgsin0pilem1  27611  stoweidlem13  27629  wallispilem4  27684  wallispi2lem1  27687  wallispi2lem2  27688  dalem10  30155  cdleme0e  30699  cdleme7c  30727  cdleme20c  30793
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421  df-ov 6043
  Copyright terms: Public domain W3C validator