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

Theorem oveq12i 6208
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 6205 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A F C )  =  ( B F D ) )
41, 2, 3mp2an 670 1  |-  ( A F C )  =  ( B F D )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1399  (class class class)co 6196
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-rex 2738  df-rab 2741  df-v 3036  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-uni 4164  df-br 4368  df-iota 5460  df-fv 5504  df-ov 6199
This theorem is referenced by:  oveq123i  6210  caovdir  6408  caovdilem  6409  caovlem2  6410  cnfcom2  8059  cnfcom2OLD  8067  canthwelem  8939  adderpqlem  9243  addassnq  9247  distrnq  9250  ltanq  9260  1lt2nq  9262  ltexnq  9264  halfnq  9265  mulcmpblnrlem  9358  mulcomsr  9377  distrsr  9379  m1p1sr  9380  m1m1sr  9381  mulgt0sr  9393  addcnsrec  9431  mulcnsrec  9432  axmulcom  9443  axmulass  9445  axdistr  9446  axi2m1  9447  addid1  9671  negdiiOLD  9817  3t3e9  10605  8th4div3  10676  halfpm6th  10677  numma  10926  4t3lem  10966  seqfeq4  12059  seqof  12067  sqdivi  12155  i4  12173  binom2i  12180  nn0opthlem1  12250  facp1  12260  fac2  12261  fac3  12262  fac4  12263  faclbnd4lem1  12273  ccat2s1len  12537  ccat2s1p2  12542  cats1len  12736  cji  12994  sqrlem5  13082  fsumadd  13563  fsumsplitsnun  13572  0.999...  13692  fprodmul  13767  fproddiv  13768  efsep  13847  ef01bndlem  13921  cos2bnd  13925  rpnnen2lem3  13952  sadeq  14124  gcdaddmlem  14168  bezout  14182  nn0gcdsq  14287  pythagtriplem16  14356  4sqlem19  14483  dec5nprm  14554  dec2nprm  14555  mod2xnegi  14559  numexp2x  14567  decsplit  14571  karatsuba  14572  2exp16  14577  37prm  14608  43prm  14609  83prm  14610  139prm  14611  163prm  14612  317prm  14613  631prm  14614  1259lem1  14615  1259lem2  14616  1259lem3  14617  1259lem4  14618  1259lem5  14619  1259prm  14620  2503lem1  14621  2503lem2  14622  2503lem3  14623  2503prm  14624  4001lem1  14625  4001lem2  14626  4001lem3  14627  4001lem4  14628  4001prm  14629  funcoppc  15281  estrchom  15513  funcestrcsetclem5  15530  yonedalem3b  15665  gsum2dlem2  17112  gsum2dOLD  17114  opprring  17393  isrhm  17483  evlsval  18301  mamudi  18990  mamudir  18991  oftpos  19039  mamutpos  19045  mdetrlin  19189  mdetrlin2  19194  mdetunilem5  19203  cpmadugsumfi  19463  cnmpt2res  20263  ussval  20847  icopnfhmeo  21528  iccpnfhmeo  21530  pcoass  21609  ovolunlem1a  21992  ioombl1lem3  22055  ioombl1lem4  22056  mbfimaopnlem  22147  iblcnlem1  22279  itgfsum  22318  iblabslem  22319  itgsplit  22327  dveflem  22465  efhalfpi  22949  efipi  22951  sin2pi  22953  ef2pi  22955  sincosq3sgn  22978  sincosq4sgn  22979  sinq34lt0t  22987  sincos4thpi  22991  tan4thpi  22992  sincos6thpi  22993  sincos3rdpi  22994  pige3  22995  cxpcn3  23209  lawcos  23266  1cubrlem  23288  quart1lem  23302  quart1  23303  asin1  23341  atancj  23357  atanlogsublem  23362  log2cnv  23391  log2tlbnd  23392  log2ublem3  23395  log2ub  23396  birthday  23401  basellem8  23478  basellem9  23479  cht2  23563  cht3  23564  1sgm2ppw  23592  bclbnd  23672  bposlem8  23683  bposlem9  23684  lgsdi  23724  lgsquadlem1  23746  mirauto  24181  axsegconlem9  24349  ax5seglem7  24359  clwlkfoclwwlk  24966  vdgr0  25021  vdegp1bi  25106  ip0i  25857  ip1ilem  25858  ip2i  25860  ipdirilem  25861  ipasslem10  25871  ip2dii  25876  pythi  25882  siilem1  25883  hvsubsub4i  26093  hvsubcan2i  26098  hisubcomi  26138  normlem0  26143  normlem1  26144  normlem2  26145  normlem3  26146  normlem6  26149  normlem8  26151  normlem9  26152  bcseqi  26154  norm-ii-i  26171  norm-iii-i  26173  normpythi  26176  norm3difi  26181  normpari  26188  normpar2i  26190  polid2i  26191  polidi  26192  bcsiALT  26213  lediri  26572  h1de2i  26588  cmcmlem  26626  cmbr2i  26631  cm2j  26655  fh3i  26658  fh4i  26659  pjaddii  26710  pjsslem  26714  pjssmii  26716  pjdifnormii  26718  lnopeq0lem1  27040  lnopunilem1  27045  lnophmlem2  27052  pjsdi2i  27192  pjclem1  27230  golem1  27306  gsumle  27923  rmulccn  28064  raddcn  28065  xrmulc1cn  28066  xrge0iifhmeo  28072  qqh0  28118  qqh1  28119  elmbfmvol2  28394  mbfmcnt  28395  eulerpartlemgvv  28498  eulerpartlemgh  28500  fib2  28524  fib3  28525  fib4  28526  fib5  28527  fib6  28528  ballotlem2  28610  ballotlemfval0  28617  ballotth  28659  ofs2  28684  problem2  29209  problem4  29211  quad3  29213  4bc2eq6  29278  halfthird  29279  5recm6rec  29280  bpoly3  29973  fsumcube  29975  iblabsnclem  30244  mzpcompact2lem  30849  pellexlem5  30934  pellfundgt1  30984  jm2.27c  31115  areaquad  31352  lhe4.4ex1a  31402  fsumsplitf  31734  fprodsplitf  31755  mccl  31772  dvnprodlem2  31910  itgsin0pilem1  31914  stoweidlem13  31961  wallispilem4  32016  wallispi2lem1  32019  wallispi2lem2  32020  dirkerper  32044  dirkertrigeqlem1  32046  fourierdlem30  32085  fourierdlem47  32102  fourierdlem103  32158  fourierdlem104  32159  fouriersw  32180  etransclem37  32220  3exp4mod41  32550  fsumsplitsndif  32664  2t6m3t4e0  33137  lincsum  33230  zlmodzxzequa  33297  zlmodzxzequap  33300  zlmodzxzldeplem3  33303  dalem10  35810  cdleme0e  36355  cdleme7c  36383  cdleme20c  36450
  Copyright terms: Public domain W3C validator