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

Theorem oveq12i 5886
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 5883 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A F C )  =  ( B F D ) )
41, 2, 3mp2an 653 1  |-  ( A F C )  =  ( B F D )
Colors of variables: wff set class
Syntax hints:    = wceq 1632  (class class class)co 5874
This theorem is referenced by:  oveq123i  5888  caovdir  6070  caovdilem  6071  caovlem2  6072  cnfcom2  7421  canthwelem  8288  adderpqlem  8594  addassnq  8598  distrnq  8601  ltanq  8611  1lt2nq  8613  ltexnq  8615  halfnq  8616  mulcmpblnrlem  8711  mulcomsr  8727  distrsr  8729  m1p1sr  8730  m1m1sr  8731  mulgt0sr  8743  addcnsrec  8781  mulcnsrec  8782  axmulcom  8793  axmulass  8795  axdistr  8796  axi2m1  8797  addid1  9008  negdii  9146  3t3e9  9889  8th4div3  9951  halfpm6th  9952  numma  10171  4t3lem  10211  seqfeq4  11111  seqof  11119  sqdivi  11204  i4  11221  binom2i  11228  binom2aiOLD  11229  nn0opthlem1  11299  facp1  11309  fac2  11310  fac3  11311  fac4  11312  faclbnd4lem1  11322  cats1len  11526  cji  11660  sqrlem5  11748  fsumadd  12227  0.999...  12353  efsep  12406  ef01bndlem  12480  cos2bnd  12484  rpnnen2lem3  12511  sadeq  12679  gcdaddmlem  12723  bezout  12737  nn0gcdsq  12839  pythagtriplem16  12899  4sqlem19  13026  dec5nprm  13097  dec2nprm  13098  mod2xnegi  13102  numexp2x  13110  decsplit  13114  karatsuba  13115  2exp16  13119  37prm  13138  43prm  13139  83prm  13140  139prm  13141  163prm  13142  317prm  13143  631prm  13144  1259lem1  13145  1259lem2  13146  1259lem3  13147  1259lem4  13148  1259lem5  13149  1259prm  13150  2503lem1  13151  2503lem2  13152  2503lem3  13153  2503prm  13154  4001lem1  13155  4001lem2  13156  4001lem3  13157  4001lem4  13158  4001prm  13159  funcoppc  13765  yonedalem3b  14069  gsum2d  15239  opprrng  15429  isrhm  15517  cnmpt2res  17387  icopnfhmeo  18457  iccpnfhmeo  18459  pcoass  18538  ovolunlem1a  18871  ioombl1lem3  18933  ioombl1lem4  18934  mbfimaopnlem  19026  iblcnlem1  19158  itgfsum  19197  iblabslem  19198  itgsplit  19206  dveflem  19342  evlsval  19419  efhalfpi  19855  efipi  19857  sin2pi  19859  ef2pi  19861  sincosq3sgn  19884  sincosq4sgn  19885  sinq34lt0t  19893  sincos4thpi  19897  tan4thpi  19898  sincos6thpi  19899  sincos3rdpi  19900  pige3  19901  cxpcn3  20104  lawcos  20130  1cubrlem  20153  quart1lem  20167  quart1  20168  asin1  20206  atancj  20222  atanlogsublem  20227  log2cnv  20256  log2tlbnd  20257  log2ublem3  20260  log2ub  20261  birthday  20265  basellem8  20341  basellem9  20342  cht2  20426  cht3  20427  1sgm2ppw  20455  bclbnd  20535  bposlem8  20546  bposlem9  20547  lgsdi  20587  lgsquadlem1  20609  ip0i  21419  ip1ilem  21420  ip2i  21422  ipdirilem  21423  ipasslem10  21433  ip2dii  21438  pythi  21444  siilem1  21445  hvsubsub4i  21654  hvsubcan2i  21659  hisubcomi  21699  normlem0  21704  normlem1  21705  normlem2  21706  normlem3  21707  normlem6  21710  normlem8  21712  normlem9  21713  bcseqi  21715  norm-ii-i  21732  norm-iii-i  21734  normpythi  21737  norm3difi  21742  normpari  21749  normpar2i  21751  polid2i  21752  polidi  21753  bcsiALT  21774  lediri  22132  h1de2i  22148  cmcmlem  22186  cmbr2i  22191  cm2j  22215  fh3i  22218  fh4i  22219  pjaddii  22270  pjsslem  22274  pjssmii  22276  pjdifnormii  22278  lnopeq0lem1  22601  lnopunilem1  22606  lnophmlem2  22613  pjsdi2i  22753  pjclem1  22791  golem1  22867  ballotlem2  23063  ballotlemfval0  23070  ballotth  23112  rmulccn  23316  raddcn  23317  xrmulc1cn  23318  xrge0iifhmeo  23333  elmbfmvol2  23587  mbfmcnt  23588  vdgr0  23907  vdegp1bi  23924  4bc2eq6  24114  halfthird  24115  5recm6rec  24116  axsegconlem9  24625  ax5seglem7  24635  bpoly3  24865  fsumcube  24867  iblabsnclem  25014  3timesi  25281  cntrset  25705  1cat  25862  prismorcset2  26021  mzpcompact2lem  26932  pellexlem5  27021  pellfundgt1  27071  jm2.27c  27203  mamudi  27564  mamudir  27565  lhe4.4ex1a  27649  itgsin0pilem1  27847  stoweidlem13  27865  wallispilem4  27920  wallispi2lem1  27923  wallispi2lem2  27924  dalem10  30484  cdleme0e  31028  cdleme7c  31056  cdleme20c  31122
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-iota 5235  df-fv 5279  df-ov 5877
  Copyright terms: Public domain W3C validator