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

Theorem oveq12i 6539
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 𝐴 = 𝐵
oveq12i.2 𝐶 = 𝐷
Assertion
Ref Expression
oveq12i (𝐴𝐹𝐶) = (𝐵𝐹𝐷)

Proof of Theorem oveq12i
StepHypRef Expression
1 oveq1i.1 . 2 𝐴 = 𝐵
2 oveq12i.2 . 2 𝐶 = 𝐷
3 oveq12 6536 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
41, 2, 3mp2an 703 1 (𝐴𝐹𝐶) = (𝐵𝐹𝐷)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  (class class class)co 6527
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rex 2901  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-iota 5754  df-fv 5798  df-ov 6530
This theorem is referenced by:  oveq123i  6541  caovdir  6743  caovdilem  6744  caovlem2  6745  cnfcom2  8459  canthwelem  9328  adderpqlem  9632  addassnq  9636  distrnq  9639  ltanq  9649  1lt2nq  9651  ltexnq  9653  halfnq  9654  mulcmpblnrlem  9747  mulcomsr  9766  distrsr  9768  m1p1sr  9769  m1m1sr  9770  mulgt0sr  9782  addcnsrec  9820  mulcnsrec  9821  axmulcom  9832  axmulass  9834  axdistr  9835  axi2m1  9836  addid1  10067  3t3e9  11027  8th4div3  11099  halfpm6th  11100  numma  11389  decmul10add  11425  decmul10addOLD  11426  4t3lem  11463  9t11e99  11503  9t11e99OLD  11504  halfthird  11517  5recm6rec  11518  fz0to3un2pr  12265  seqfeq4  12667  seqof  12675  sqdivi  12765  sq4e2t8  12779  i4  12784  binom2i  12791  nn0opthlem1  12872  facp1  12882  fac2  12883  fac3  12884  fac4  12885  faclbnd4lem1  12897  4bc2eq6  12933  ccat2s1len  13199  ccat2s1p2  13204  cats1len  13402  cats2cat  13404  ofs2  13504  cji  13693  sqrlem5  13781  fsumadd  14263  fsumsplitsnun  14274  0.999...  14397  0.999...OLD  14398  fprodmul  14475  fproddiv  14476  fprodsplitf  14504  bpoly3  14574  fsumcube  14576  efsep  14625  ef01bndlem  14699  cos2bnd  14703  rpnnen2lem3  14730  3dvds2dec  14840  3dvds2decOLD  14841  flodddiv4  14921  sadeq  14978  gcdaddmlem  15029  bezout  15044  nn0gcdsq  15244  pythagtriplem16  15319  4sqlem19  15451  dec5nprm  15554  dec2nprm  15555  mod2xnegi  15559  numexp2x  15567  decsplit  15571  decsplitOLD  15575  karatsuba  15576  karatsubaOLD  15577  2exp16  15581  37prm  15612  43prm  15613  83prm  15614  139prm  15615  163prm  15616  317prm  15617  631prm  15618  1259lem1  15622  1259lem2  15623  1259lem3  15624  1259lem4  15625  1259lem5  15626  1259prm  15627  2503lem1  15628  2503lem2  15629  2503lem3  15630  2503prm  15631  4001lem1  15632  4001lem2  15633  4001lem3  15634  4001lem4  15635  4001prm  15636  funcoppc  16304  estrchom  16536  funcestrcsetclem5  16553  yonedalem3b  16688  gsum2dlem2  18139  opprring  18400  isrhm  18490  evlsval  19286  mamudi  19970  mamudir  19971  oftpos  20019  mamutpos  20025  mdetrlin  20169  mdetrlin2  20174  mdetunilem5  20183  cpmadugsumfi  20443  cnmpt2res  21232  ussval  21815  icopnfhmeo  22481  iccpnfhmeo  22483  pcoass  22563  ovolunlem1a  22988  ioombl1lem3  23052  ioombl1lem4  23053  mbfimaopnlem  23145  iblcnlem1  23277  itgfsum  23316  iblabslem  23317  itgsplit  23325  dveflem  23463  efhalfpi  23944  efipi  23946  sin2pi  23948  ef2pi  23950  sincosq3sgn  23973  sincosq4sgn  23974  sinq34lt0t  23982  sincos4thpi  23986  tan4thpi  23987  sincos6thpi  23988  sincos3rdpi  23989  pige3  23990  cxpcn3  24206  lawcos  24263  1cubrlem  24285  quart1lem  24299  quart1  24300  asin1  24338  atancj  24354  atanlogsublem  24359  log2cnv  24388  log2tlbnd  24389  log2ublem3  24392  log2ub  24393  birthday  24398  basellem8  24531  basellem9  24532  cht2  24615  cht3  24616  1sgm2ppw  24642  bclbnd  24722  bposlem8  24733  bposlem9  24734  lgsdi  24776  lgsquadlem1  24822  2lgsoddprmlem3c  24854  2lgsoddprmlem3d  24855  mirauto  25297  axsegconlem9  25523  ax5seglem7  25533  clwlkfoclwwlk  26138  vdgr0  26193  vdegp1bi  26278  ex-exp  26465  ex-fac  26466  ex-bc  26467  ex-hash  26468  ip0i  26870  ip1ilem  26871  ip2i  26873  ipdirilem  26874  ipasslem10  26884  ip2dii  26889  pythi  26895  siilem1  26896  hvsubsub4i  27106  hvsubcan2i  27111  hisubcomi  27151  normlem0  27156  normlem1  27157  normlem2  27158  normlem3  27159  normlem6  27162  normlem8  27164  normlem9  27165  bcseqi  27167  norm-ii-i  27184  norm-iii-i  27186  normpythi  27189  norm3difi  27194  normpari  27201  normpar2i  27203  polid2i  27204  polidi  27205  bcsiALT  27226  lediri  27586  h1de2i  27602  cmcmlem  27640  cmbr2i  27645  cm2j  27669  fh3i  27672  fh4i  27673  pjaddii  27724  pjsslem  27728  pjssmii  27730  pjdifnormii  27732  lnopeq0lem1  28054  lnopunilem1  28059  lnophmlem2  28066  pjsdi2i  28206  pjclem1  28244  golem1  28320  gsumle  28916  rmulccn  29108  raddcn  29109  xrmulc1cn  29110  xrge0iifhmeo  29116  qqh0  29162  qqh1  29163  elmbfmvol2  29462  mbfmcnt  29463  eulerpartlemgvv  29571  eulerpartlemgh  29573  fib2  29597  fib3  29598  fib4  29599  fib5  29600  fib6  29601  ballotlem2  29683  ballotlemfval0  29690  ballotth  29732  problem2  30619  problem2OLD  30620  problem4  30622  quad3  30624  pigt3  32368  poimirlem30  32405  iblabsnclem  32439  dalem10  33773  cdleme0e  34318  cdleme7c  34346  cdleme20c  34413  mzpcompact2lem  36128  pellexlem5  36211  pellfundgt1  36261  jm2.27c  36388  areaquad  36617  lhe4.4ex1a  37346  fsumsplitf  38431  mccl  38462  dvnprodlem2  38634  itgsin0pilem1  38638  stoweidlem13  38703  wallispilem4  38758  wallispi2lem1  38761  wallispi2lem2  38762  dirkerper  38786  dirkertrigeqlem1  38788  fourierdlem30  38827  fourierdlem47  38843  fourierdlem103  38899  fourierdlem104  38900  fouriersw  38921  etransclem37  38961  sge0splitmpt  39101  sge0xaddlem2  39124  sge0xadd  39125  caragen0  39193  caragenuncllem  39199  2exp5  39843  139prmALT  39847  127prm  39851  2exp11  39853  m11nprm  39854  3exp4mod41  39869  fsumsplitsndif  40215  clwlksfoclwwlk  41265  eupth2eucrct  41380  2t6m3t4e0  41914  lincsum  42007  zlmodzxzequa  42074  zlmodzxzequap  42077  zlmodzxzldeplem3  42080
  Copyright terms: Public domain W3C validator