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

Theorem oveq1d 5527
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 5519 . 2 (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
31, 2syl 14 1 (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1243  (class class class)co 5512
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-rex 2312  df-v 2559  df-un 2922  df-sn 3381  df-pr 3382  df-op 3384  df-uni 3581  df-br 3765  df-iota 4867  df-fv 4910  df-ov 5515
This theorem is referenced by:  csbov2g  5546  caovassg  5659  caovdig  5675  caovdirg  5678  caov12d  5682  caov31d  5683  caov411d  5686  grprinvlem  5695  grprinvd  5696  grpridd  5697  caofinvl  5733  omsuc  6051  nnmsucr  6067  nnm1  6097  nnm2  6098  ecovass  6215  ecoviass  6216  ecovdi  6217  ecovidi  6218  addasspig  6426  mulasspig  6428  mulpipq2  6467  distrnqg  6483  ltsonq  6494  ltanqg  6496  ltmnqg  6497  ltexnqq  6504  archnqq  6513  prarloclemarch2  6515  enq0sym  6528  addnq0mo  6543  mulnq0mo  6544  addnnnq0  6545  nqpnq0nq  6549  nq0m0r  6552  nq0a0  6553  nnanq0  6554  distrnq0  6555  addassnq0  6558  addpinq1  6560  prarloclemlo  6590  prarloclem3  6593  prarloclem5  6596  prarloclemcalc  6598  addnqprllem  6623  addnqprulem  6624  appdivnq  6659  recexprlem1ssl  6729  recexprlem1ssu  6730  ltmprr  6738  cauappcvgprlemladdru  6752  cauappcvgprlem1  6755  caucvgprlemnkj  6762  caucvgprlemnbj  6763  caucvgprlemcl  6772  caucvgprlemladdfu  6773  caucvgprlemladdrl  6774  caucvgprlem1  6775  caucvgprprlemcbv  6783  caucvgprprlemval  6784  caucvgprprlemexb  6803  caucvgprprlem1  6805  addcmpblnr  6822  mulcmpblnrlemg  6823  addsrmo  6826  mulsrmo  6827  addsrpr  6828  mulsrpr  6829  ltsrprg  6830  1idsr  6851  pn0sr  6854  recexgt0sr  6856  mulgt0sr  6860  srpospr  6865  prsradd  6868  caucvgsrlemfv  6873  caucvgsrlemcau  6875  caucvgsrlemgt1  6877  caucvgsrlemoffval  6878  caucvgsrlemoffcau  6880  caucvgsrlemoffres  6882  caucvgsrlembnd  6883  caucvgsr  6884  pitonnlem1p1  6920  pitonnlem2  6921  pitonn  6922  recidpirqlemcalc  6931  ax1rid  6949  axrnegex  6951  axcnre  6953  recriota  6962  nntopi  6966  axcaucvglemval  6969  axcaucvglemcau  6970  axcaucvglemres  6971  mul12  7140  mul4  7143  muladd11  7144  readdcan  7151  add12  7167  cnegex  7187  addcan  7189  negeu  7200  pncan2  7216  addsubass  7219  addsub  7220  2addsub  7223  addsubeq4  7224  subid  7228  subid1  7229  npncan  7230  nppcan  7231  nnpcan  7232  nnncan1  7245  npncan3  7247  pnpcan  7248  pnncan  7250  ppncan  7251  addsub4  7252  negsub  7257  subneg  7258  ine0  7389  mulneg1  7390  ltadd2  7414  apreap  7576  cru  7591  recexap  7632  mulcanapd  7640  div23ap  7668  div13ap  7670  divcanap4  7674  divsubdirap  7682  divmuldivap  7686  divdivdivap  7687  divcanap5  7688  divmul13ap  7689  divmuleqap  7691  divdiv32ap  7694  divcanap7  7695  dmdcanap  7696  divdivap1  7697  divdivap2  7698  divadddivap  7701  divsubdivap  7702  conjmulap  7703  divneg2ap  7710  mvllmulapd  7807  lt2mul2div  7843  nndivtr  7953  2halves  8152  halfaddsub  8157  avgle1  8163  avgle2  8164  div4p1lem1div2  8175  un0addcl  8213  un0mulcl  8214  peano2z  8279  zneo  8337  nneoor  8338  nneo  8339  zeo  8341  zeo2  8342  deceq1  8368  qreccl  8574  lincmb01cmp  8869  iccf1o  8870  fzosubel3  9050  2tnp1ge0ge0  9141  fldiv4p1lem1div2  9145  ceilqm1lt  9152  frecuzrdgsuc  9175  frecfzennn  9177  iseqovex  9193  iseq1p  9213  iseqcaopr2  9215  iseqcaopr  9216  iseqid  9221  iseqhomo  9222  expp1  9236  exprecap  9270  expaddzaplem  9272  expmulzap  9275  expdivap  9279  sqval  9286  sqsubswap  9288  subsq  9332  subsq2  9333  binom2  9336  binom2sub  9338  binom3  9340  zesq  9341  bernneq2  9344  reval  9423  crre  9431  remim  9434  remul2  9447  immul2  9454  imval2  9468  cjdivap  9483  caucvgre  9554  cvg1nlemcau  9557  cvg1nlemres  9558  resqrexlemp1rp  9578  resqrexlemfp1  9581  resqrexlemover  9582  resqrexlemcalc1  9586  resqrexlemcalc3  9588  resqrexlemnm  9590  resqrexlemoverl  9593  resqrexlemglsq  9594  resqrexlemga  9595  resqrexlemsqa  9596  resqrexlemex  9597  resqrex  9598  sqrtdiv  9614  absvalsq  9625  absreimsq  9639  absdivap  9642  cau3lem  9684  clim  9775  clim2  9777  climshftlemg  9796  climshft2  9800  climcn1  9802  climcn2  9803  subcn2  9805  climmulc2  9824  climsubc2  9826  clim2iser  9830  climcau  9839  serif0  9844  sqr2irrlem  9850
  Copyright terms: Public domain W3C validator