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

Theorem oveq12i 6825
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 6822 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
41, 2, 3mp2an 710 1 (𝐴𝐹𝐶) = (𝐵𝐹𝐷)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1632  (class class class)co 6813
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-iota 6012  df-fv 6057  df-ov 6816
This theorem is referenced by:  oveq123i  6827  caovdir  7033  caovdilem  7034  caovlem2  7035  cnfcom2  8772  canthwelem  9664  adderpqlem  9968  addassnq  9972  distrnq  9975  ltanq  9985  1lt2nq  9987  ltexnq  9989  halfnq  9990  mulcmpblnrlem  10083  mulcomsr  10102  distrsr  10104  m1p1sr  10105  m1m1sr  10106  mulgt0sr  10118  addcnsrec  10156  mulcnsrec  10157  axmulcom  10168  axmulass  10170  axdistr  10171  axi2m1  10172  addid1  10408  3t3e9  11372  8th4div3  11444  halfpm6th  11445  numma  11749  decmul10add  11785  decmul10addOLD  11786  4t3lem  11823  9t11e99  11863  9t11e99OLD  11864  halfthird  11877  5recm6rec  11878  fz0to3un2pr  12635  seqfeq4  13044  seqof  13052  sqdivi  13142  sq4e2t8  13156  i4  13161  binom2i  13168  nn0opthlem1  13249  facp1  13259  fac2  13260  fac3  13261  fac4  13262  faclbnd4lem1  13274  4bc2eq6  13310  ccat2s1len  13596  ccat2s1p2  13604  cats1len  13805  cats2cat  13807  ofs2  13911  cji  14098  sqrlem5  14186  fsumadd  14669  fsumsplitf  14671  fsumsplitsnun  14683  fsumsplitsnunOLD  14685  0.999...  14811  0.999...OLD  14812  fprodmul  14889  fproddiv  14890  fprodsplitf  14918  bpoly3  14988  fsumcube  14990  efsep  15039  ef01bndlem  15113  cos2bnd  15117  rpnnen2lem3  15144  3dvds2dec  15258  3dvds2decOLD  15259  flodddiv4  15339  sadeq  15396  gcdaddmlem  15447  bezout  15462  nn0gcdsq  15662  pythagtriplem16  15737  4sqlem19  15869  dec5nprm  15972  dec2nprm  15973  mod2xnegi  15977  numexp2x  15985  decsplit  15989  decsplitOLD  15993  karatsuba  15994  karatsubaOLD  15995  2exp16  15999  37prm  16030  43prm  16031  83prm  16032  139prm  16033  163prm  16034  317prm  16035  631prm  16036  1259lem1  16040  1259lem2  16041  1259lem3  16042  1259lem4  16043  1259lem5  16044  1259prm  16045  2503lem1  16046  2503lem2  16047  2503lem3  16048  2503prm  16049  4001lem1  16050  4001lem2  16051  4001lem3  16052  4001lem4  16053  4001prm  16054  funcoppc  16736  estrchom  16968  funcestrcsetclem5  16985  yonedalem3b  17120  gsum2dlem2  18570  opprring  18831  isrhm  18923  evlsval  19721  mamudi  20411  mamudir  20412  oftpos  20460  mamutpos  20466  mdetrlin  20610  mdetrlin2  20615  mdetunilem5  20624  cpmadugsumfi  20884  cnmpt2res  21682  ussval  22264  icopnfhmeo  22943  iccpnfhmeo  22945  pcoass  23024  ovolunlem1a  23464  ioombl1lem3  23528  ioombl1lem4  23529  mbfimaopnlem  23621  iblcnlem1  23753  itgfsum  23792  iblabslem  23793  itgsplit  23801  dveflem  23941  efhalfpi  24422  efipi  24424  sin2pi  24426  ef2pi  24428  sincosq3sgn  24451  sincosq4sgn  24452  sinq34lt0t  24460  sincos4thpi  24464  tan4thpi  24465  sincos6thpi  24466  sincos3rdpi  24467  pige3  24468  cxpcn3  24688  lawcos  24745  1cubrlem  24767  quart1lem  24781  quart1  24782  asin1  24820  atancj  24836  atanlogsublem  24841  log2cnv  24870  log2tlbnd  24871  log2ublem3  24874  log2ub  24875  birthday  24880  basellem8  25013  basellem9  25014  cht2  25097  cht3  25098  1sgm2ppw  25124  bclbnd  25204  bposlem8  25215  bposlem9  25216  lgsdi  25258  lgsquadlem1  25304  2lgsoddprmlem3c  25336  2lgsoddprmlem3d  25337  mirauto  25778  axsegconlem9  26004  ax5seglem7  26014  vtxdginducedm1  26649  clwlkclwwlkfo  27132  clwlksfoclwwlkOLD  27217  eupth2eucrct  27369  ex-exp  27618  ex-fac  27619  ex-bc  27620  ex-hash  27621  ip0i  27989  ip1ilem  27990  ip2i  27992  ipdirilem  27993  ipasslem10  28003  ip2dii  28008  pythi  28014  siilem1  28015  hvsubsub4i  28225  hvsubcan2i  28230  hisubcomi  28270  normlem0  28275  normlem1  28276  normlem2  28277  normlem3  28278  normlem6  28281  normlem8  28283  normlem9  28284  bcseqi  28286  norm-ii-i  28303  norm-iii-i  28305  normpythi  28308  norm3difi  28313  normpari  28320  normpar2i  28322  polid2i  28323  polidi  28324  bcsiALT  28345  lediri  28705  h1de2i  28721  cmcmlem  28759  cmbr2i  28764  cm2j  28788  fh3i  28791  fh4i  28792  pjaddii  28843  pjsslem  28847  pjssmii  28849  pjdifnormii  28851  lnopeq0lem1  29173  lnopunilem1  29178  lnophmlem2  29185  pjsdi2i  29325  pjclem1  29363  golem1  29439  dpmul100  29914  dpmul1000  29916  dpadd2  29927  dpadd  29928  dpadd3  29929  dpmul  29930  dpmul4  29931  gsumle  30088  rmulccn  30283  raddcn  30284  xrmulc1cn  30285  xrge0iifhmeo  30291  qqh0  30337  qqh1  30338  elmbfmvol2  30638  mbfmcnt  30639  eulerpartlemgvv  30747  eulerpartlemgh  30749  fib2  30773  fib3  30774  fib4  30775  fib5  30776  fib6  30777  ballotlem2  30859  ballotlemfval0  30866  ballotth  30908  hgt750lem2  31039  problem2  31866  problem2OLD  31867  problem4  31869  quad3  31871  pigt3  33715  poimirlem30  33752  iblabsnclem  33786  dalem10  35462  cdleme0e  36007  cdleme7c  36035  cdleme20c  36101  mzpcompact2lem  37816  pellexlem5  37899  pellfundgt1  37949  jm2.27c  38076  areaquad  38304  lhe4.4ex1a  39030  mccl  40333  dvnprodlem2  40665  itgsin0pilem1  40668  stoweidlem13  40733  wallispilem4  40788  wallispi2lem1  40791  wallispi2lem2  40792  dirkerper  40816  dirkertrigeqlem1  40818  fourierdlem30  40857  fourierdlem47  40873  fourierdlem103  40929  fourierdlem104  40930  fouriersw  40951  etransclem37  40991  sge0splitmpt  41131  sge0xaddlem2  41154  sge0xadd  41155  caragen0  41226  caragenuncllem  41232  fsumsplitsndif  41853  2exp5  42017  139prmALT  42021  127prm  42025  2exp11  42027  m11nprm  42028  3exp4mod41  42043  sbgoldbo  42185  2t6m3t4e0  42636  lincsum  42728  zlmodzxzequa  42795  zlmodzxzequap  42798  zlmodzxzldeplem3  42801
  Copyright terms: Public domain W3C validator