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

Theorem oveq12i 5870
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 5867 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A F C )  =  ( B F D ) )
41, 2, 3mp2an 653 1  |-  ( A F C )  =  ( B F D )
Colors of variables: wff set class
Syntax hints:    = wceq 1623  (class class class)co 5858
This theorem is referenced by:  oveq123i  5872  caovdir  6054  caovdilem  6055  caovlem2  6056  cnfcom2  7405  canthwelem  8272  adderpqlem  8578  addassnq  8582  distrnq  8585  ltanq  8595  1lt2nq  8597  ltexnq  8599  halfnq  8600  mulcmpblnrlem  8695  mulcomsr  8711  distrsr  8713  m1p1sr  8714  m1m1sr  8715  mulgt0sr  8727  addcnsrec  8765  mulcnsrec  8766  axmulcom  8777  axmulass  8779  axdistr  8780  axi2m1  8781  addid1  8992  negdii  9130  3t3e9  9873  8th4div3  9935  halfpm6th  9936  numma  10155  4t3lem  10195  seqfeq4  11095  seqof  11103  sqdivi  11188  i4  11205  binom2i  11212  binom2aiOLD  11213  nn0opthlem1  11283  facp1  11293  fac2  11294  fac3  11295  fac4  11296  faclbnd4lem1  11306  cats1len  11510  cji  11644  sqrlem5  11732  fsumadd  12211  0.999...  12337  efsep  12390  ef01bndlem  12464  cos2bnd  12468  rpnnen2lem3  12495  sadeq  12663  gcdaddmlem  12707  bezout  12721  nn0gcdsq  12823  pythagtriplem16  12883  4sqlem19  13010  dec5nprm  13081  dec2nprm  13082  mod2xnegi  13086  numexp2x  13094  decsplit  13098  karatsuba  13099  2exp16  13103  37prm  13122  43prm  13123  83prm  13124  139prm  13125  163prm  13126  317prm  13127  631prm  13128  1259lem1  13129  1259lem2  13130  1259lem3  13131  1259lem4  13132  1259lem5  13133  1259prm  13134  2503lem1  13135  2503lem2  13136  2503lem3  13137  2503prm  13138  4001lem1  13139  4001lem2  13140  4001lem3  13141  4001lem4  13142  4001prm  13143  funcoppc  13749  yonedalem3b  14053  gsum2d  15223  opprrng  15413  isrhm  15501  cnmpt2res  17371  icopnfhmeo  18441  iccpnfhmeo  18443  pcoass  18522  ovolunlem1a  18855  ioombl1lem3  18917  ioombl1lem4  18918  mbfimaopnlem  19010  iblcnlem1  19142  itgfsum  19181  iblabslem  19182  itgsplit  19190  dveflem  19326  evlsval  19403  efhalfpi  19839  efipi  19841  sin2pi  19843  ef2pi  19845  sincosq3sgn  19868  sincosq4sgn  19869  sinq34lt0t  19877  sincos4thpi  19881  tan4thpi  19882  sincos6thpi  19883  sincos3rdpi  19884  pige3  19885  cxpcn3  20088  lawcos  20114  1cubrlem  20137  quart1lem  20151  quart1  20152  asin1  20190  atancj  20206  atanlogsublem  20211  log2cnv  20240  log2tlbnd  20241  log2ublem3  20244  log2ub  20245  birthday  20249  basellem8  20325  basellem9  20326  cht2  20410  cht3  20411  1sgm2ppw  20439  bclbnd  20519  bposlem8  20530  bposlem9  20531  lgsdi  20571  lgsquadlem1  20593  ip0i  21403  ip1ilem  21404  ip2i  21406  ipdirilem  21407  ipasslem10  21417  ip2dii  21422  pythi  21428  siilem1  21429  hvsubsub4i  21638  hvsubcan2i  21643  hisubcomi  21683  normlem0  21688  normlem1  21689  normlem2  21690  normlem3  21691  normlem6  21694  normlem8  21696  normlem9  21697  bcseqi  21699  norm-ii-i  21716  norm-iii-i  21718  normpythi  21721  norm3difi  21726  normpari  21733  normpar2i  21735  polid2i  21736  polidi  21737  bcsiALT  21758  lediri  22116  h1de2i  22132  cmcmlem  22170  cmbr2i  22175  cm2j  22199  fh3i  22202  fh4i  22203  pjaddii  22254  pjsslem  22258  pjssmii  22260  pjdifnormii  22262  lnopeq0lem1  22585  lnopunilem1  22590  lnophmlem2  22597  pjsdi2i  22737  pjclem1  22775  golem1  22851  ballotlem2  23047  ballotlemfval0  23054  ballotth  23096  rmulccn  23301  raddcn  23302  xrmulc1cn  23303  xrge0iifhmeo  23318  elmbfmvol2  23572  mbfmcnt  23573  vdgr0  23892  vdegp1bi  23909  4bc2eq6  24099  halfthird  24100  5recm6rec  24101  axsegconlem9  24553  ax5seglem7  24563  bpoly3  24793  fsumcube  24795  3timesi  25178  cntrset  25602  1cat  25759  prismorcset2  25918  mzpcompact2lem  26829  pellexlem5  26918  pellfundgt1  26968  jm2.27c  27100  mamudi  27461  mamudir  27462  lhe4.4ex1a  27546  itgsin0pilem1  27744  stoweidlem13  27762  wallispilem4  27817  wallispi2lem1  27820  wallispi2lem2  27821  dalem10  29862  cdleme0e  30406  cdleme7c  30434  cdleme20c  30500
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-ov 5861
  Copyright terms: Public domain W3C validator