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

Theorem oveq12i 6095
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 6092 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A F C )  =  ( B F D ) )
41, 2, 3mp2an 655 1  |-  ( A F C )  =  ( B F D )
Colors of variables: wff set class
Syntax hints:    = wceq 1653  (class class class)co 6083
This theorem is referenced by:  oveq123i  6097  caovdir  6283  caovdilem  6284  caovlem2  6285  cnfcom2  7661  canthwelem  8527  adderpqlem  8833  addassnq  8837  distrnq  8840  ltanq  8850  1lt2nq  8852  ltexnq  8854  halfnq  8855  mulcmpblnrlem  8950  mulcomsr  8966  distrsr  8968  m1p1sr  8969  m1m1sr  8970  mulgt0sr  8982  addcnsrec  9020  mulcnsrec  9021  axmulcom  9032  axmulass  9034  axdistr  9035  axi2m1  9036  addid1  9248  negdii  9386  3t3e9  10131  8th4div3  10193  halfpm6th  10194  numma  10415  4t3lem  10455  seqfeq4  11374  seqof  11382  sqdivi  11468  i4  11485  binom2i  11492  binom2aiOLD  11493  nn0opthlem1  11563  facp1  11573  fac2  11574  fac3  11575  fac4  11576  faclbnd4lem1  11586  cats1len  11826  cji  11966  sqrlem5  12054  fsumadd  12534  0.999...  12660  efsep  12713  ef01bndlem  12787  cos2bnd  12791  rpnnen2lem3  12818  sadeq  12986  gcdaddmlem  13030  bezout  13044  nn0gcdsq  13146  pythagtriplem16  13206  4sqlem19  13333  dec5nprm  13404  dec2nprm  13405  mod2xnegi  13409  numexp2x  13417  decsplit  13421  karatsuba  13422  2exp16  13426  37prm  13445  43prm  13446  83prm  13447  139prm  13448  163prm  13449  317prm  13450  631prm  13451  1259lem1  13452  1259lem2  13453  1259lem3  13454  1259lem4  13455  1259lem5  13456  1259prm  13457  2503lem1  13458  2503lem2  13459  2503lem3  13460  2503prm  13461  4001lem1  13462  4001lem2  13463  4001lem3  13464  4001lem4  13465  4001prm  13466  funcoppc  14074  yonedalem3b  14378  gsum2d  15548  opprrng  15738  isrhm  15826  cnmpt2res  17711  ussval  18291  icopnfhmeo  18970  iccpnfhmeo  18972  pcoass  19051  ovolunlem1a  19394  ioombl1lem3  19456  ioombl1lem4  19457  mbfimaopnlem  19549  iblcnlem1  19681  itgfsum  19720  iblabslem  19721  itgsplit  19729  dveflem  19865  evlsval  19942  efhalfpi  20381  efipi  20383  sin2pi  20385  ef2pi  20387  sincosq3sgn  20410  sincosq4sgn  20411  sinq34lt0t  20419  sincos4thpi  20423  tan4thpi  20424  sincos6thpi  20425  sincos3rdpi  20426  pige3  20427  cxpcn3  20634  lawcos  20660  1cubrlem  20683  quart1lem  20697  quart1  20698  asin1  20736  atancj  20752  atanlogsublem  20757  log2cnv  20786  log2tlbnd  20787  log2ublem3  20790  log2ub  20791  birthday  20795  basellem8  20872  basellem9  20873  cht2  20957  cht3  20958  1sgm2ppw  20986  bclbnd  21066  bposlem8  21077  bposlem9  21078  lgsdi  21118  lgsquadlem1  21140  vdgr0  21673  vdegp1bi  21709  ip0i  22328  ip1ilem  22329  ip2i  22331  ipdirilem  22332  ipasslem10  22342  ip2dii  22347  pythi  22353  siilem1  22354  hvsubsub4i  22563  hvsubcan2i  22568  hisubcomi  22608  normlem0  22613  normlem1  22614  normlem2  22615  normlem3  22616  normlem6  22619  normlem8  22621  normlem9  22622  bcseqi  22624  norm-ii-i  22641  norm-iii-i  22643  normpythi  22646  norm3difi  22651  normpari  22658  normpar2i  22660  polid2i  22661  polidi  22662  bcsiALT  22683  lediri  23041  h1de2i  23057  cmcmlem  23095  cmbr2i  23100  cm2j  23124  fh3i  23127  fh4i  23128  pjaddii  23179  pjsslem  23183  pjssmii  23185  pjdifnormii  23187  lnopeq0lem1  23510  lnopunilem1  23515  lnophmlem2  23522  pjsdi2i  23662  pjclem1  23700  golem1  23776  rmulccn  24316  raddcn  24317  xrmulc1cn  24318  xrge0iifhmeo  24324  qqh0  24370  qqh1  24371  elmbfmvol2  24619  mbfmcnt  24620  ballotlem2  24748  ballotlemfval0  24755  ballotth  24797  4bc2eq6  25206  halfthird  25207  5recm6rec  25208  fprodmul  25286  fproddiv  25287  axsegconlem9  25866  ax5seglem7  25876  bpoly3  26106  fsumcube  26108  iblabsnclem  26270  mzpcompact2lem  26810  pellexlem5  26898  pellfundgt1  26948  jm2.27c  27080  mamudi  27440  mamudir  27441  lhe4.4ex1a  27525  itgsin0pilem1  27722  stoweidlem13  27740  wallispilem4  27795  wallispi2lem1  27798  wallispi2lem2  27799  dalem10  30472  cdleme0e  31016  cdleme7c  31044  cdleme20c  31110
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rex 2713  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4215  df-iota 5420  df-fv 5464  df-ov 6086
  Copyright terms: Public domain W3C validator