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

Theorem oveq12i 6092
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 6089 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A F C )  =  ( B F D ) )
41, 2, 3mp2an 665 1  |-  ( A F C )  =  ( B F D )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1362  (class class class)co 6080
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-iota 5369  df-fv 5414  df-ov 6083
This theorem is referenced by:  oveq123i  6094  caovdir  6286  caovdilem  6287  caovlem2  6288  cnfcom2  7923  cnfcom2OLD  7931  canthwelem  8805  adderpqlem  9111  addassnq  9115  distrnq  9118  ltanq  9128  1lt2nq  9130  ltexnq  9132  halfnq  9133  mulcmpblnrlem  9228  mulcomsr  9244  distrsr  9246  m1p1sr  9247  m1m1sr  9248  mulgt0sr  9260  addcnsrec  9298  mulcnsrec  9299  axmulcom  9310  axmulass  9312  axdistr  9313  axi2m1  9314  addid1  9537  negdii  9680  3t3e9  10462  8th4div3  10533  halfpm6th  10534  numma  10774  4t3lem  10814  seqfeq4  11839  seqof  11847  sqdivi  11934  i4  11952  binom2i  11959  binom2aiOLD  11960  nn0opthlem1  12030  facp1  12040  fac2  12041  fac3  12042  fac4  12043  faclbnd4lem1  12053  cats1len  12471  cji  12632  sqrlem5  12720  fsumadd  13199  0.999...  13324  efsep  13377  ef01bndlem  13451  cos2bnd  13455  rpnnen2lem3  13482  sadeq  13651  gcdaddmlem  13695  bezout  13709  nn0gcdsq  13813  pythagtriplem16  13880  4sqlem19  14007  dec5nprm  14078  dec2nprm  14079  mod2xnegi  14083  numexp2x  14091  decsplit  14095  karatsuba  14096  2exp16  14100  37prm  14131  43prm  14132  83prm  14133  139prm  14134  163prm  14135  317prm  14136  631prm  14137  1259lem1  14138  1259lem2  14139  1259lem3  14140  1259lem4  14141  1259lem5  14142  1259prm  14143  2503lem1  14144  2503lem2  14145  2503lem3  14146  2503prm  14147  4001lem1  14148  4001lem2  14149  4001lem3  14150  4001lem4  14151  4001prm  14152  funcoppc  14768  yonedalem3b  15072  gsum2dlem2  16436  gsum2dOLD  16438  opprrng  16657  isrhm  16745  mamudi  18149  mamudir  18150  oftpos  18175  mamutpos  18185  mdetrlin  18251  mdetrlin2  18255  mdetunilem5  18264  cnmpt2res  19092  ussval  19676  icopnfhmeo  20357  iccpnfhmeo  20359  pcoass  20438  ovolunlem1a  20821  ioombl1lem3  20883  ioombl1lem4  20884  mbfimaopnlem  20975  iblcnlem1  21107  itgfsum  21146  iblabslem  21147  itgsplit  21155  dveflem  21293  evlsval  21371  efhalfpi  21818  efipi  21820  sin2pi  21822  ef2pi  21824  sincosq3sgn  21847  sincosq4sgn  21848  sinq34lt0t  21856  sincos4thpi  21860  tan4thpi  21861  sincos6thpi  21862  sincos3rdpi  21863  pige3  21864  cxpcn3  22071  lawcos  22097  1cubrlem  22121  quart1lem  22135  quart1  22136  asin1  22174  atancj  22190  atanlogsublem  22195  log2cnv  22224  log2tlbnd  22225  log2ublem3  22228  log2ub  22229  birthday  22233  basellem8  22310  basellem9  22311  cht2  22395  cht3  22396  1sgm2ppw  22424  bclbnd  22504  bposlem8  22515  bposlem9  22516  lgsdi  22556  lgsquadlem1  22578  axsegconlem9  22994  ax5seglem7  23004  vdgr0  23393  vdegp1bi  23429  ip0i  24048  ip1ilem  24049  ip2i  24051  ipdirilem  24052  ipasslem10  24062  ip2dii  24067  pythi  24073  siilem1  24074  hvsubsub4i  24284  hvsubcan2i  24289  hisubcomi  24329  normlem0  24334  normlem1  24335  normlem2  24336  normlem3  24337  normlem6  24340  normlem8  24342  normlem9  24343  bcseqi  24345  norm-ii-i  24362  norm-iii-i  24364  normpythi  24367  norm3difi  24372  normpari  24379  normpar2i  24381  polid2i  24382  polidi  24383  bcsiALT  24404  lediri  24763  h1de2i  24779  cmcmlem  24817  cmbr2i  24822  cm2j  24846  fh3i  24849  fh4i  24850  pjaddii  24901  pjsslem  24905  pjssmii  24907  pjdifnormii  24909  lnopeq0lem1  25232  lnopunilem1  25237  lnophmlem2  25244  pjsdi2i  25384  pjclem1  25422  golem1  25498  gsumle  26098  gsummptun  26100  rmulccn  26212  raddcn  26213  xrmulc1cn  26214  xrge0iifhmeo  26220  qqh0  26267  qqh1  26268  elmbfmvol2  26536  mbfmcnt  26537  eulerpartlemgvv  26607  eulerpartlemgh  26609  fib2  26633  fib3  26634  fib4  26635  fib5  26636  fib6  26637  ballotlem2  26719  ballotlemfval0  26726  ballotth  26768  ofs2  26793  signstfveq0  26826  problem2  27147  problem4  27149  4bc2eq6  27238  halfthird  27239  5recm6rec  27240  fprodmul  27318  fproddiv  27319  bpoly3  28048  fsumcube  28050  iblabsnclem  28299  mzpcompact2lem  28933  pellexlem5  29019  pellfundgt1  29069  jm2.27c  29201  areaquad  29437  lhe4.4ex1a  29448  itgsin0pilem1  29636  stoweidlem13  29654  wallispilem4  29709  wallispi2lem1  29712  wallispi2lem2  29713  fsumsplitsndif  30084  fsumsplitsnun  30088  ccat2s1len  30110  ccat2s1p2  30112  clwlkfoclwwlk  30364  2t6m3t4e0  30585  lincsum  30693  zlmodzxzequa  30768  zlmodzxzequap  30771  zlmodzxzldeplem3  30774  dalem10  32911  cdleme0e  33455  cdleme7c  33483  cdleme20c  33549
  Copyright terms: Public domain W3C validator