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

Theorem oveq12i 6296
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 6293 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A F C )  =  ( B F D ) )
41, 2, 3mp2an 672 1  |-  ( A F C )  =  ( B F D )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379  (class class class)co 6284
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-iota 5551  df-fv 5596  df-ov 6287
This theorem is referenced by:  oveq123i  6298  caovdir  6493  caovdilem  6494  caovlem2  6495  cnfcom2  8146  cnfcom2OLD  8154  canthwelem  9028  adderpqlem  9332  addassnq  9336  distrnq  9339  ltanq  9349  1lt2nq  9351  ltexnq  9353  halfnq  9354  mulcmpblnrlem  9447  mulcomsr  9466  distrsr  9468  m1p1sr  9469  m1m1sr  9470  mulgt0sr  9482  addcnsrec  9520  mulcnsrec  9521  axmulcom  9532  axmulass  9534  axdistr  9535  axi2m1  9536  addid1  9759  negdii  9903  3t3e9  10688  8th4div3  10759  halfpm6th  10760  numma  11007  4t3lem  11047  seqfeq4  12124  seqof  12132  sqdivi  12220  i4  12238  binom2i  12245  binom2aiOLD  12246  nn0opthlem1  12316  facp1  12326  fac2  12327  fac3  12328  fac4  12329  faclbnd4lem1  12339  ccat2s1len  12591  ccat2s1p2  12596  cats1len  12788  cji  12955  sqrlem5  13043  fsumadd  13524  fsumsplitsnun  13533  0.999...  13653  efsep  13706  ef01bndlem  13780  cos2bnd  13784  rpnnen2lem3  13811  sadeq  13981  gcdaddmlem  14025  bezout  14039  nn0gcdsq  14144  pythagtriplem16  14213  4sqlem19  14340  dec5nprm  14411  dec2nprm  14412  mod2xnegi  14416  numexp2x  14424  decsplit  14428  karatsuba  14429  2exp16  14433  37prm  14464  43prm  14465  83prm  14466  139prm  14467  163prm  14468  317prm  14469  631prm  14470  1259lem1  14471  1259lem2  14472  1259lem3  14473  1259lem4  14474  1259lem5  14475  1259prm  14476  2503lem1  14477  2503lem2  14478  2503lem3  14479  2503prm  14480  4001lem1  14481  4001lem2  14482  4001lem3  14483  4001lem4  14484  4001prm  14485  funcoppc  15102  yonedalem3b  15406  gsum2dlem2  16801  gsum2dOLD  16803  opprrng  17081  isrhm  17171  evlsval  17987  mamudi  18700  mamudir  18701  oftpos  18749  mamutpos  18755  mdetrlin  18899  mdetrlin2  18904  mdetunilem5  18913  cpmadugsumfi  19173  cnmpt2res  19941  ussval  20525  icopnfhmeo  21206  iccpnfhmeo  21208  pcoass  21287  ovolunlem1a  21670  ioombl1lem3  21733  ioombl1lem4  21734  mbfimaopnlem  21825  iblcnlem1  21957  itgfsum  21996  iblabslem  21997  itgsplit  22005  dveflem  22143  efhalfpi  22625  efipi  22627  sin2pi  22629  ef2pi  22631  sincosq3sgn  22654  sincosq4sgn  22655  sinq34lt0t  22663  sincos4thpi  22667  tan4thpi  22668  sincos6thpi  22669  sincos3rdpi  22670  pige3  22671  cxpcn3  22878  lawcos  22904  1cubrlem  22928  quart1lem  22942  quart1  22943  asin1  22981  atancj  22997  atanlogsublem  23002  log2cnv  23031  log2tlbnd  23032  log2ublem3  23035  log2ub  23036  birthday  23040  basellem8  23117  basellem9  23118  cht2  23202  cht3  23203  1sgm2ppw  23231  bclbnd  23311  bposlem8  23322  bposlem9  23323  lgsdi  23363  lgsquadlem1  23385  mirauto  23797  axsegconlem9  23932  ax5seglem7  23942  clwlkfoclwwlk  24549  vdgr0  24604  vdegp1bi  24689  ip0i  25444  ip1ilem  25445  ip2i  25447  ipdirilem  25448  ipasslem10  25458  ip2dii  25463  pythi  25469  siilem1  25470  hvsubsub4i  25680  hvsubcan2i  25685  hisubcomi  25725  normlem0  25730  normlem1  25731  normlem2  25732  normlem3  25733  normlem6  25736  normlem8  25738  normlem9  25739  bcseqi  25741  norm-ii-i  25758  norm-iii-i  25760  normpythi  25763  norm3difi  25768  normpari  25775  normpar2i  25777  polid2i  25778  polidi  25779  bcsiALT  25800  lediri  26159  h1de2i  26175  cmcmlem  26213  cmbr2i  26218  cm2j  26242  fh3i  26245  fh4i  26246  pjaddii  26297  pjsslem  26301  pjssmii  26303  pjdifnormii  26305  lnopeq0lem1  26628  lnopunilem1  26633  lnophmlem2  26640  pjsdi2i  26780  pjclem1  26818  golem1  26894  gsumle  27461  rmulccn  27574  raddcn  27575  xrmulc1cn  27576  xrge0iifhmeo  27582  qqh0  27629  qqh1  27630  elmbfmvol2  27906  mbfmcnt  27907  eulerpartlemgvv  27983  eulerpartlemgh  27985  fib2  28009  fib3  28010  fib4  28011  fib5  28012  fib6  28013  ballotlem2  28095  ballotlemfval0  28102  ballotth  28144  ofs2  28169  signstfveq0  28202  problem2  28523  problem4  28525  quad3  28527  4bc2eq6  28615  halfthird  28616  5recm6rec  28617  fprodmul  28695  fproddiv  28696  bpoly3  29425  fsumcube  29427  iblabsnclem  29683  mzpcompact2lem  30316  pellexlem5  30401  pellfundgt1  30451  jm2.27c  30581  areaquad  30817  lhe4.4ex1a  30862  itgsin0pilem1  31295  stoweidlem13  31341  wallispilem4  31396  wallispi2lem1  31399  wallispi2lem2  31400  dirkerper  31424  dirkertrigeqlem1  31426  fourierdlem30  31465  fourierdlem47  31482  fourierdlem103  31538  fourierdlem104  31539  fouriersw  31560  fsumsplitsndif  31841  2t6m3t4e0  32033  lincsum  32129  zlmodzxzequa  32196  zlmodzxzequap  32199  zlmodzxzldeplem3  32202  dalem10  34487  cdleme0e  35031  cdleme7c  35059  cdleme20c  35125
  Copyright terms: Public domain W3C validator