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

Theorem oveq12i 6293
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 6290 . 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 1383  (class class class)co 6281
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rex 2799  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-iota 5541  df-fv 5586  df-ov 6284
This theorem is referenced by:  oveq123i  6295  caovdir  6494  caovdilem  6495  caovlem2  6496  cnfcom2  8149  cnfcom2OLD  8157  canthwelem  9031  adderpqlem  9335  addassnq  9339  distrnq  9342  ltanq  9352  1lt2nq  9354  ltexnq  9356  halfnq  9357  mulcmpblnrlem  9450  mulcomsr  9469  distrsr  9471  m1p1sr  9472  m1m1sr  9473  mulgt0sr  9485  addcnsrec  9523  mulcnsrec  9524  axmulcom  9535  axmulass  9537  axdistr  9538  axi2m1  9539  addid1  9763  negdiiOLD  9909  3t3e9  10695  8th4div3  10766  halfpm6th  10767  numma  11017  4t3lem  11057  seqfeq4  12138  seqof  12146  sqdivi  12234  i4  12252  binom2i  12259  binom2aiOLD  12260  nn0opthlem1  12330  facp1  12340  fac2  12341  fac3  12342  fac4  12343  faclbnd4lem1  12353  ccat2s1len  12610  ccat2s1p2  12615  cats1len  12807  cji  12974  sqrlem5  13062  fsumadd  13543  fsumsplitsnun  13552  0.999...  13672  fprodmul  13747  fproddiv  13748  efsep  13827  ef01bndlem  13901  cos2bnd  13905  rpnnen2lem3  13932  sadeq  14104  gcdaddmlem  14148  bezout  14162  nn0gcdsq  14267  pythagtriplem16  14336  4sqlem19  14463  dec5nprm  14534  dec2nprm  14535  mod2xnegi  14539  numexp2x  14547  decsplit  14551  karatsuba  14552  2exp16  14557  37prm  14588  43prm  14589  83prm  14590  139prm  14591  163prm  14592  317prm  14593  631prm  14594  1259lem1  14595  1259lem2  14596  1259lem3  14597  1259lem4  14598  1259lem5  14599  1259prm  14600  2503lem1  14601  2503lem2  14602  2503lem3  14603  2503prm  14604  4001lem1  14605  4001lem2  14606  4001lem3  14607  4001lem4  14608  4001prm  14609  funcoppc  15223  yonedalem3b  15527  gsum2dlem2  16977  gsum2dOLD  16979  opprring  17259  isrhm  17349  evlsval  18167  mamudi  18883  mamudir  18884  oftpos  18932  mamutpos  18938  mdetrlin  19082  mdetrlin2  19087  mdetunilem5  19096  cpmadugsumfi  19356  cnmpt2res  20156  ussval  20740  icopnfhmeo  21421  iccpnfhmeo  21423  pcoass  21502  ovolunlem1a  21885  ioombl1lem3  21948  ioombl1lem4  21949  mbfimaopnlem  22040  iblcnlem1  22172  itgfsum  22211  iblabslem  22212  itgsplit  22220  dveflem  22358  efhalfpi  22842  efipi  22844  sin2pi  22846  ef2pi  22848  sincosq3sgn  22871  sincosq4sgn  22872  sinq34lt0t  22880  sincos4thpi  22884  tan4thpi  22885  sincos6thpi  22886  sincos3rdpi  22887  pige3  22888  cxpcn3  23100  lawcos  23126  1cubrlem  23150  quart1lem  23164  quart1  23165  asin1  23203  atancj  23219  atanlogsublem  23224  log2cnv  23253  log2tlbnd  23254  log2ublem3  23257  log2ub  23258  birthday  23262  basellem8  23339  basellem9  23340  cht2  23424  cht3  23425  1sgm2ppw  23453  bclbnd  23533  bposlem8  23544  bposlem9  23545  lgsdi  23585  lgsquadlem1  23607  mirauto  24039  axsegconlem9  24206  ax5seglem7  24216  clwlkfoclwwlk  24823  vdgr0  24878  vdegp1bi  24963  ip0i  25718  ip1ilem  25719  ip2i  25721  ipdirilem  25722  ipasslem10  25732  ip2dii  25737  pythi  25743  siilem1  25744  hvsubsub4i  25954  hvsubcan2i  25959  hisubcomi  25999  normlem0  26004  normlem1  26005  normlem2  26006  normlem3  26007  normlem6  26010  normlem8  26012  normlem9  26013  bcseqi  26015  norm-ii-i  26032  norm-iii-i  26034  normpythi  26037  norm3difi  26042  normpari  26049  normpar2i  26051  polid2i  26052  polidi  26053  bcsiALT  26074  lediri  26433  h1de2i  26449  cmcmlem  26487  cmbr2i  26492  cm2j  26516  fh3i  26519  fh4i  26520  pjaddii  26571  pjsslem  26575  pjssmii  26577  pjdifnormii  26579  lnopeq0lem1  26902  lnopunilem1  26907  lnophmlem2  26914  pjsdi2i  27054  pjclem1  27092  golem1  27168  gsumle  27748  rmulccn  27888  raddcn  27889  xrmulc1cn  27890  xrge0iifhmeo  27896  qqh0  27943  qqh1  27944  elmbfmvol2  28216  mbfmcnt  28217  eulerpartlemgvv  28293  eulerpartlemgh  28295  fib2  28319  fib3  28320  fib4  28321  fib5  28322  fib6  28323  ballotlem2  28405  ballotlemfval0  28412  ballotth  28454  ofs2  28479  signstfveq0  28512  problem2  28998  problem4  29000  quad3  29002  4bc2eq6  29090  halfthird  29091  5recm6rec  29092  bpoly3  29796  fsumcube  29798  iblabsnclem  30054  mzpcompact2lem  30660  pellexlem5  30745  pellfundgt1  30795  jm2.27c  30925  areaquad  31160  lhe4.4ex1a  31210  fsumsplitf  31522  fprodsplitf  31543  mccl  31560  dvnprodlem2  31698  itgsin0pilem1  31702  stoweidlem13  31749  wallispilem4  31804  wallispi2lem1  31807  wallispi2lem2  31808  dirkerper  31832  dirkertrigeqlem1  31834  fourierdlem30  31873  fourierdlem47  31890  fourierdlem103  31946  fourierdlem104  31947  fouriersw  31968  etransclem37  32008  fsumsplitsndif  32300  estrchom  32599  funcestrcsetclem5  32616  2t6m3t4e0  32805  lincsum  32900  zlmodzxzequa  32967  zlmodzxzequap  32970  zlmodzxzldeplem3  32973  dalem10  35272  cdleme0e  35817  cdleme7c  35845  cdleme20c  35912
  Copyright terms: Public domain W3C validator