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

Theorem oveq1d 5630
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 5622 . 2 (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
31, 2syl 14 1 (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1287  (class class class)co 5615
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-3an 924  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-rex 2361  df-v 2617  df-un 2992  df-sn 3437  df-pr 3438  df-op 3440  df-uni 3639  df-br 3823  df-iota 4948  df-fv 4991  df-ov 5618
This theorem is referenced by:  csbov2g  5649  caovassg  5762  caovdig  5778  caovdirg  5781  caov12d  5785  caov31d  5786  caov411d  5789  grprinvlem  5798  grprinvd  5799  grpridd  5800  caofinvl  5836  omsuc  6189  nnmsucr  6205  nnm1  6237  nnm2  6238  ecovass  6355  ecoviass  6356  ecovdi  6357  ecovidi  6358  addasspig  6836  mulasspig  6838  mulpipq2  6877  distrnqg  6893  ltsonq  6904  ltanqg  6906  ltmnqg  6907  ltexnqq  6914  archnqq  6923  prarloclemarch2  6925  enq0sym  6938  addnq0mo  6953  mulnq0mo  6954  addnnnq0  6955  nqpnq0nq  6959  nq0m0r  6962  nq0a0  6963  nnanq0  6964  distrnq0  6965  addassnq0  6968  addpinq1  6970  prarloclemlo  7000  prarloclem3  7003  prarloclem5  7006  prarloclemcalc  7008  addnqprllem  7033  addnqprulem  7034  appdivnq  7069  recexprlem1ssl  7139  recexprlem1ssu  7140  ltmprr  7148  cauappcvgprlemladdru  7162  cauappcvgprlem1  7165  caucvgprlemnkj  7172  caucvgprlemnbj  7173  caucvgprlemcl  7182  caucvgprlemladdfu  7183  caucvgprlemladdrl  7184  caucvgprlem1  7185  caucvgprprlemcbv  7193  caucvgprprlemval  7194  caucvgprprlemexb  7213  caucvgprprlem1  7215  addcmpblnr  7232  mulcmpblnrlemg  7233  addsrmo  7236  mulsrmo  7237  addsrpr  7238  mulsrpr  7239  ltsrprg  7240  1idsr  7261  pn0sr  7264  recexgt0sr  7266  mulgt0sr  7270  srpospr  7275  prsradd  7278  caucvgsrlemfv  7283  caucvgsrlemcau  7285  caucvgsrlemgt1  7287  caucvgsrlemoffval  7288  caucvgsrlemoffcau  7290  caucvgsrlemoffres  7292  caucvgsrlembnd  7293  caucvgsr  7294  pitonnlem1p1  7330  pitonnlem2  7331  pitonn  7332  recidpirqlemcalc  7341  ax1rid  7359  axrnegex  7361  axcnre  7363  recriota  7372  nntopi  7376  axcaucvglemval  7379  axcaucvglemcau  7380  axcaucvglemres  7381  mul12  7558  mul4  7561  muladd11  7562  readdcan  7569  muladd11r  7585  add12  7587  cnegex  7607  addcan  7609  negeu  7620  pncan2  7636  addsubass  7639  addsub  7640  2addsub  7643  addsubeq4  7644  subid  7648  subid1  7649  npncan  7650  nppcan  7651  nnpcan  7652  nnncan1  7665  npncan3  7667  pnpcan  7668  pnncan  7670  ppncan  7671  addsub4  7672  negsub  7677  subneg  7678  mvlraddd  7792  mvrraddd  7793  subaddeqd  7794  ine0  7819  mulneg1  7820  ltadd2  7844  apreap  8008  cru  8023  recexap  8064  mulcanapd  8072  div23ap  8100  div13ap  8102  divmulassap  8104  divmulasscomap  8105  divcanap4  8108  muldivdirap  8116  divsubdirap  8117  divmuldivap  8121  divdivdivap  8122  divcanap5  8123  divmul13ap  8124  divmuleqap  8126  divdiv32ap  8129  divcanap7  8130  dmdcanap  8131  divdivap1  8132  divdivap2  8133  divadddivap  8136  divsubdivap  8137  conjmulap  8138  divneg2ap  8145  mvllmulapd  8242  lt2mul2div  8278  nndivtr  8401  2halves  8581  halfaddsub  8586  avgle1  8592  avgle2  8593  div4p1lem1div2  8605  un0addcl  8642  un0mulcl  8643  peano2z  8722  zneo  8783  nneoor  8784  nneo  8785  zeo  8787  zeo2  8788  deceq1  8816  qreccl  9062  lincmb01cmp  9355  iccf1o  9356  fzosubel3  9538  qavgle  9601  2tnp1ge0ge0  9639  fldiv4p1lem1div2  9643  ceilqm1lt  9650  flqdiv  9659  modqlt  9671  modqdiffl  9673  modqcyc2  9698  modqaddabs  9700  mulqaddmodid  9702  mulp1mod1  9703  modqmuladd  9704  modqmuladdnn0  9706  qnegmod  9707  addmodid  9710  addmodidr  9711  modqadd2mod  9712  modqm1p1mod0  9713  modqmul12d  9716  modqnegd  9717  modqadd12d  9718  modqsub12d  9719  q2submod  9723  modqmulmodr  9728  modqaddmulmod  9729  modqsubdir  9731  modfzo0difsn  9733  modsumfzodifsn  9734  addmodlteq  9736  frecuzrdgsuc  9752  frecfzennn  9764  iseqovex  9801  iseqoveq  9816  iseq1p  9833  iseqcaopr2  9835  iseqcaopr  9836  iseqid  9862  iseqhomo  9864  iseqz  9865  expp1  9882  exprecap  9916  expaddzaplem  9918  expmulzap  9921  expdivap  9926  sqval  9933  sqsubswap  9935  subsq  9980  subsq2  9981  binom2  9984  binom2sub  9986  mulbinom2  9988  binom3  9989  zesq  9990  bernneq2  9993  sqoddm1div8  10024  nn0opthlem1d  10046  nn0opthd  10048  nn0opth2d  10049  facp1  10056  facdiv  10064  facndiv  10065  faclbnd  10067  faclbnd2  10068  faclbnd3  10069  bcval  10075  bccmpl  10080  bcm1k  10086  bcp1n  10087  bcp1nk  10088  ibcval5  10089  bcp1m1  10091  bcpasc  10092  bcn2m1  10095  hashprg  10134  hashdifpr  10146  hashfzo  10148  hashfzp1  10150  hashfz0  10151  hashxp  10152  zfz1isolemsplit  10161  zfz1isolem1  10163  iseqcoll  10165  reval  10200  crre  10208  remim  10211  remul2  10224  immul2  10231  imval2  10245  cjdivap  10260  caucvgre  10331  cvg1nlemcau  10334  cvg1nlemres  10335  resqrexlemp1rp  10356  resqrexlemfp1  10359  resqrexlemover  10360  resqrexlemcalc1  10364  resqrexlemcalc3  10366  resqrexlemnm  10368  resqrexlemoverl  10371  resqrexlemglsq  10372  resqrexlemga  10373  resqrexlemsqa  10374  resqrexlemex  10375  resqrex  10376  sqrtdiv  10392  absvalsq  10403  absreimsq  10417  absdivap  10420  cau3lem  10464  maxabslemlub  10557  maxabslemval  10558  max0addsup  10569  clim  10585  clim2  10587  climshftlemg  10606  climshft2  10611  climcn1  10613  climcn2  10614  subcn2  10616  climmulc2  10635  climsubc2  10637  clim2iser  10641  climcau  10650  serif0  10655  fzosump1  10717  fsum1p  10718  fsump1  10720  moddvds  10730  mulmoddvds  10789  3dvds2dec  10791  zeo3  10793  odd2np1lem  10797  odd2np1  10798  oexpneg  10802  2tp1odd  10809  ltoddhalfle  10818  opoe  10820  opeo  10822  omeo  10823  m1expo  10825  m1exp1  10826  nn0o1gt2  10830  nn0o  10832  divalglemnn  10843  divalglemqt  10844  divalglemeunn  10846  divalglemex  10847  divalglemeuneg  10848  flodddiv4  10859  flodddiv4t2lthalf  10862  gcdaddm  10900  bezoutlemnewy  10910  bezoutlema  10913  bezoutlemb  10914  bezoutlemex  10915  bezoutlemaz  10917  mulgcd  10930  gcddiv  10933  gcdmultiplez  10935  rpmulgcd  10940  rplpwr  10941  lcmgcdlem  10984  lcmgcd  10985  divgcdcoprmex  11009  cncongr2  11011  prmexpb  11055  rpexp  11057  rpexp1i  11058  sqrt2irrlem  11065  oddpwdclemxy  11072  oddpwdclemndvds  11074  sqpweven  11078  2sqpwodd  11079  sqne2sq  11080  qmuldeneqnum  11098  nn0gcdsq  11103  zgcdsq  11104  numdensq  11105  dfphi2  11121  phiprmpw  11123  phiprm  11124  hashgcdlem  11128
  Copyright terms: Public domain W3C validator