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

Theorem oveq12i 6315
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 6312 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A F C )  =  ( B F D ) )
41, 2, 3mp2an 677 1  |-  ( A F C )  =  ( B F D )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1438  (class class class)co 6303
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-rex 2782  df-rab 2785  df-v 3084  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-if 3911  df-sn 3998  df-pr 4000  df-op 4004  df-uni 4218  df-br 4422  df-iota 5563  df-fv 5607  df-ov 6306
This theorem is referenced by:  oveq123i  6317  caovdir  6515  caovdilem  6516  caovlem2  6517  cnfcom2  8210  canthwelem  9077  adderpqlem  9381  addassnq  9385  distrnq  9388  ltanq  9398  1lt2nq  9400  ltexnq  9402  halfnq  9403  mulcmpblnrlem  9496  mulcomsr  9515  distrsr  9517  m1p1sr  9518  m1m1sr  9519  mulgt0sr  9531  addcnsrec  9569  mulcnsrec  9570  axmulcom  9581  axmulass  9583  axdistr  9584  axi2m1  9585  addid1  9815  negdiiOLD  9961  3t3e9  10764  8th4div3  10835  halfpm6th  10836  numma  11084  4t3lem  11124  halfthird  11159  5recm6rec  11160  seqfeq4  12263  seqof  12271  sqdivi  12360  i4  12378  binom2i  12385  nn0opthlem1  12455  facp1  12465  fac2  12466  fac3  12467  fac4  12468  faclbnd4lem1  12479  4bc2eq6  12515  ccat2s1len  12753  ccat2s1p2  12758  cats1len  12952  cji  13216  sqrlem5  13304  fsumadd  13798  fsumsplitsnun  13809  0.999...  13930  fprodmul  14007  fproddiv  14008  fprodsplitf  14035  bpoly3  14104  fsumcube  14106  efsep  14157  ef01bndlem  14231  cos2bnd  14235  rpnnen2lem3  14262  sadeq  14439  gcdaddmlem  14485  bezout  14503  nn0gcdsq  14694  pythagtriplem16  14773  4sqlem19  14906  dec5nprm  15031  dec2nprm  15032  mod2xnegi  15036  numexp2x  15044  decsplit  15048  karatsuba  15049  2exp16  15054  37prm  15085  43prm  15086  83prm  15087  139prm  15088  163prm  15089  317prm  15090  631prm  15091  1259lem1  15095  1259lem2  15096  1259lem3  15097  1259lem4  15098  1259lem5  15099  1259prm  15100  2503lem1  15101  2503lem2  15102  2503lem3  15103  2503prm  15104  4001lem1  15105  4001lem2  15106  4001lem3  15107  4001lem4  15108  4001prm  15109  funcoppc  15773  estrchom  16005  funcestrcsetclem5  16022  yonedalem3b  16157  gsum2dlem2  17596  opprring  17852  isrhm  17942  evlsval  18735  mamudi  19420  mamudir  19421  oftpos  19469  mamutpos  19475  mdetrlin  19619  mdetrlin2  19624  mdetunilem5  19633  cpmadugsumfi  19893  cnmpt2res  20684  ussval  21266  icopnfhmeo  21963  iccpnfhmeo  21965  pcoass  22047  ovolunlem1a  22441  ioombl1lem3  22505  ioombl1lem4  22506  mbfimaopnlem  22603  iblcnlem1  22737  itgfsum  22776  iblabslem  22777  itgsplit  22785  dveflem  22923  efhalfpi  23418  efipi  23420  sin2pi  23422  ef2pi  23424  sincosq3sgn  23447  sincosq4sgn  23448  sinq34lt0t  23456  sincos4thpi  23460  tan4thpi  23461  sincos6thpi  23462  sincos3rdpi  23463  pige3  23464  cxpcn3  23680  lawcos  23737  1cubrlem  23759  quart1lem  23773  quart1  23774  asin1  23812  atancj  23828  atanlogsublem  23833  log2cnv  23862  log2tlbnd  23863  log2ublem3  23866  log2ub  23867  birthday  23872  basellem8  24006  basellem9  24007  cht2  24091  cht3  24092  1sgm2ppw  24120  bclbnd  24200  bposlem8  24211  bposlem9  24212  lgsdi  24252  lgsquadlem1  24274  mirauto  24721  axsegconlem9  24947  ax5seglem7  24957  clwlkfoclwwlk  25565  vdgr0  25620  vdegp1bi  25705  ip0i  26458  ip1ilem  26459  ip2i  26461  ipdirilem  26462  ipasslem10  26472  ip2dii  26477  pythi  26483  siilem1  26484  hvsubsub4i  26704  hvsubcan2i  26709  hisubcomi  26749  normlem0  26754  normlem1  26755  normlem2  26756  normlem3  26757  normlem6  26760  normlem8  26762  normlem9  26763  bcseqi  26765  norm-ii-i  26782  norm-iii-i  26784  normpythi  26787  norm3difi  26792  normpari  26799  normpar2i  26801  polid2i  26802  polidi  26803  bcsiALT  26824  lediri  27182  h1de2i  27198  cmcmlem  27236  cmbr2i  27241  cm2j  27265  fh3i  27268  fh4i  27269  pjaddii  27320  pjsslem  27324  pjssmii  27326  pjdifnormii  27328  lnopeq0lem1  27650  lnopunilem1  27655  lnophmlem2  27662  pjsdi2i  27802  pjclem1  27840  golem1  27916  gsumle  28543  rmulccn  28736  raddcn  28737  xrmulc1cn  28738  xrge0iifhmeo  28744  qqh0  28790  qqh1  28791  elmbfmvol2  29091  mbfmcnt  29092  eulerpartlemgvv  29211  eulerpartlemgh  29213  fib2  29237  fib3  29238  fib4  29239  fib5  29240  fib6  29241  ballotlem2  29323  ballotlemfval0  29330  ballotth  29372  ballotthOLD  29410  ofs2  29435  problem2  30300  problem4  30302  quad3  30304  pigt3  31896  poimirlem30  31928  iblabsnclem  31963  dalem10  33201  cdleme0e  33746  cdleme7c  33774  cdleme20c  33841  mzpcompact2lem  35556  pellexlem5  35641  pellfundgt1  35695  jm2.27c  35826  areaquad  36065  lhe4.4ex1a  36580  fsumsplitf  37513  mccl  37542  dvnprodlem2  37686  itgsin0pilem1  37690  stoweidlem13  37737  wallispilem4  37794  wallispi2lem1  37797  wallispi2lem2  37798  dirkerper  37822  dirkertrigeqlem1  37824  fourierdlem30  37863  fourierdlem47  37881  fourierdlem103  37937  fourierdlem104  37938  fouriersw  37959  etransclem37  38000  sge0splitmpt  38085  sge0xaddlem2  38108  sge0xadd  38109  caragen0  38150  caragenuncllem  38156  3exp4mod41  38672  fsumsplitsndif  38800  2t6m3t4e0  39473  lincsum  39566  zlmodzxzequa  39633  zlmodzxzequap  39636  zlmodzxzldeplem3  39639
  Copyright terms: Public domain W3C validator