ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  oveq1d GIF version

Theorem oveq1d 5555
Description: Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.)
Hypothesis
Ref Expression
oveq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
oveq1d (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))

Proof of Theorem oveq1d
StepHypRef Expression
1 oveq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 oveq1 5547 . 2 (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
31, 2syl 14 1 (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1259  (class class class)co 5540
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-3an 898  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-rex 2329  df-v 2576  df-un 2950  df-sn 3409  df-pr 3410  df-op 3412  df-uni 3609  df-br 3793  df-iota 4895  df-fv 4938  df-ov 5543
This theorem is referenced by:  csbov2g  5574  caovassg  5687  caovdig  5703  caovdirg  5706  caov12d  5710  caov31d  5711  caov411d  5714  grprinvlem  5723  grprinvd  5724  grpridd  5725  caofinvl  5761  omsuc  6082  nnmsucr  6098  nnm1  6128  nnm2  6129  ecovass  6246  ecoviass  6247  ecovdi  6248  ecovidi  6249  addasspig  6486  mulasspig  6488  mulpipq2  6527  distrnqg  6543  ltsonq  6554  ltanqg  6556  ltmnqg  6557  ltexnqq  6564  archnqq  6573  prarloclemarch2  6575  enq0sym  6588  addnq0mo  6603  mulnq0mo  6604  addnnnq0  6605  nqpnq0nq  6609  nq0m0r  6612  nq0a0  6613  nnanq0  6614  distrnq0  6615  addassnq0  6618  addpinq1  6620  prarloclemlo  6650  prarloclem3  6653  prarloclem5  6656  prarloclemcalc  6658  addnqprllem  6683  addnqprulem  6684  appdivnq  6719  recexprlem1ssl  6789  recexprlem1ssu  6790  ltmprr  6798  cauappcvgprlemladdru  6812  cauappcvgprlem1  6815  caucvgprlemnkj  6822  caucvgprlemnbj  6823  caucvgprlemcl  6832  caucvgprlemladdfu  6833  caucvgprlemladdrl  6834  caucvgprlem1  6835  caucvgprprlemcbv  6843  caucvgprprlemval  6844  caucvgprprlemexb  6863  caucvgprprlem1  6865  addcmpblnr  6882  mulcmpblnrlemg  6883  addsrmo  6886  mulsrmo  6887  addsrpr  6888  mulsrpr  6889  ltsrprg  6890  1idsr  6911  pn0sr  6914  recexgt0sr  6916  mulgt0sr  6920  srpospr  6925  prsradd  6928  caucvgsrlemfv  6933  caucvgsrlemcau  6935  caucvgsrlemgt1  6937  caucvgsrlemoffval  6938  caucvgsrlemoffcau  6940  caucvgsrlemoffres  6942  caucvgsrlembnd  6943  caucvgsr  6944  pitonnlem1p1  6980  pitonnlem2  6981  pitonn  6982  recidpirqlemcalc  6991  ax1rid  7009  axrnegex  7011  axcnre  7013  recriota  7022  nntopi  7026  axcaucvglemval  7029  axcaucvglemcau  7030  axcaucvglemres  7031  mul12  7203  mul4  7206  muladd11  7207  readdcan  7214  muladd11r  7230  add12  7232  cnegex  7252  addcan  7254  negeu  7265  pncan2  7281  addsubass  7284  addsub  7285  2addsub  7288  addsubeq4  7289  subid  7293  subid1  7294  npncan  7295  nppcan  7296  nnpcan  7297  nnncan1  7310  npncan3  7312  pnpcan  7313  pnncan  7315  ppncan  7316  addsub4  7317  negsub  7322  subneg  7323  mvlraddd  7437  mvrraddd  7438  subaddeqd  7439  ine0  7463  mulneg1  7464  ltadd2  7488  apreap  7652  cru  7667  recexap  7708  mulcanapd  7716  div23ap  7744  div13ap  7746  divcanap4  7750  muldivdirap  7758  divsubdirap  7759  divmuldivap  7763  divdivdivap  7764  divcanap5  7765  divmul13ap  7766  divmuleqap  7768  divdiv32ap  7771  divcanap7  7772  dmdcanap  7773  divdivap1  7774  divdivap2  7775  divadddivap  7778  divsubdivap  7779  conjmulap  7780  divneg2ap  7787  mvllmulapd  7884  lt2mul2div  7920  nndivtr  8031  2halves  8211  halfaddsub  8216  avgle1  8222  avgle2  8223  div4p1lem1div2  8235  un0addcl  8272  un0mulcl  8273  peano2z  8338  zneo  8398  nneoor  8399  nneo  8400  zeo  8402  zeo2  8403  deceq1  8431  qreccl  8674  lincmb01cmp  8972  iccf1o  8973  fzosubel3  9154  qavgle  9215  2tnp1ge0ge0  9251  fldiv4p1lem1div2  9255  ceilqm1lt  9262  flqdiv  9271  modqlt  9283  modqdiffl  9285  modqcyc2  9310  modqaddabs  9312  mulqaddmodid  9314  mulp1mod1  9315  modqmuladd  9316  modqmuladdnn0  9318  qnegmod  9319  addmodid  9322  addmodidr  9323  modqadd2mod  9324  modqm1p1mod0  9325  modqmul12d  9328  modqnegd  9329  modqadd12d  9330  modqsub12d  9331  q2submod  9335  modqmulmodr  9340  modqaddmulmod  9341  modqsubdir  9343  modfzo0difsn  9345  modsumfzodifsn  9346  addmodlteq  9348  frecuzrdgsuc  9365  frecfzennn  9367  iseqovex  9383  iseq1p  9403  iseqcaopr2  9405  iseqcaopr  9406  iseqid  9411  iseqhomo  9412  iseqz  9413  expp1  9427  exprecap  9461  expaddzaplem  9463  expmulzap  9466  expdivap  9471  sqval  9478  sqsubswap  9480  subsq  9525  subsq2  9526  binom2  9529  binom2sub  9531  mulbinom2  9533  binom3  9534  zesq  9535  bernneq2  9538  sqoddm1div8  9569  nn0opthlem1d  9588  nn0opthd  9590  nn0opth2d  9591  facp1  9598  facdiv  9606  facndiv  9607  faclbnd  9609  faclbnd2  9610  faclbnd3  9611  bcval  9617  bccmpl  9622  bcm1k  9628  bcp1n  9629  bcp1nk  9630  ibcval5  9631  bcp1m1  9633  bcpasc  9634  bcn2m1  9637  reval  9677  crre  9685  remim  9688  remul2  9701  immul2  9708  imval2  9722  cjdivap  9737  caucvgre  9808  cvg1nlemcau  9811  cvg1nlemres  9812  resqrexlemp1rp  9833  resqrexlemfp1  9836  resqrexlemover  9837  resqrexlemcalc1  9841  resqrexlemcalc3  9843  resqrexlemnm  9845  resqrexlemoverl  9848  resqrexlemglsq  9849  resqrexlemga  9850  resqrexlemsqa  9851  resqrexlemex  9852  resqrex  9853  sqrtdiv  9869  absvalsq  9880  absreimsq  9894  absdivap  9897  cau3lem  9941  clim  10033  clim2  10035  climshftlemg  10054  climshft2  10058  climcn1  10060  climcn2  10061  subcn2  10063  climmulc2  10082  climsubc2  10084  clim2iser  10088  climcau  10097  serif0  10102  moddvds  10117  mulmoddvds  10175  3dvds2dec  10177  zeo3  10179  odd2np1lem  10183  odd2np1  10184  oexpneg  10188  2tp1odd  10196  ltoddhalfle  10205  opoe  10207  opeo  10209  omeo  10210  m1expo  10212  m1exp1  10213  nn0o1gt2  10217  nn0o  10219  divalglemnn  10230  divalglemqt  10231  divalglemeunn  10233  divalglemex  10234  divalglemeuneg  10235  flodddiv4  10246  flodddiv4t2lthalf  10249  sqr2irrlem  10250  oddpwdclemxy  10257  oddpwdclemndvds  10259
  Copyright terms: Public domain W3C validator