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

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

Proof of Theorem oveq2d
StepHypRef Expression
1 oveq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 oveq2 5621 . 2 (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
31, 2syl 14 1 (𝜑 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1287  (class class class)co 5613
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 3637  df-br 3821  df-iota 4946  df-fv 4989  df-ov 5616
This theorem is referenced by:  csbov1g  5646  caovassg  5760  caovdig  5776  caovdirg  5779  caov32d  5782  caov4d  5786  caov42d  5788  grprinvlem  5796  grprinvd  5797  grpridd  5798  nnaass  6200  nndi  6201  nnmass  6202  nnmsucr  6203  ecovass  6353  ecoviass  6354  ecovdi  6355  ecovidi  6356  addasspig  6833  mulasspig  6835  distrpig  6836  dfplpq2  6857  mulpipq2  6874  addassnqg  6885  prarloclemarch  6921  prarloclemarch2  6922  ltrnqg  6923  enq0sym  6935  addnq0mo  6950  mulnq0mo  6951  addnnnq0  6952  nq0a0  6960  distrnq0  6962  addassnq0  6965  prarloclemlo  6997  prarloclem3  7000  prarloclem5  7003  prarloclemcalc  7005  addnqprl  7032  addnqpru  7033  prmuloclemcalc  7068  mulnqprl  7071  mulnqpru  7072  distrlem4prl  7087  distrlem4pru  7088  1idprl  7093  1idpru  7094  ltexprlemloc  7110  addcanprleml  7117  addcanprlemu  7118  recexprlem1ssu  7137  ltmprr  7145  caucvgprlemcanl  7147  cauappcvgprlemladdru  7159  cauappcvgprlemladdrl  7160  cauappcvgprlem1  7162  cauappcvgprlemlim  7164  caucvgprlemnkj  7169  caucvgprlemnbj  7170  caucvgprlemdisj  7177  caucvgprlemloc  7178  caucvgprlemcl  7179  caucvgprlemladdrl  7181  caucvgprlem1  7182  caucvgpr  7185  caucvgprprlemell  7188  caucvgprprlemcbv  7190  caucvgprprlemval  7191  caucvgprprlemnkeqj  7193  caucvgprprlemopl  7200  caucvgprprlemlol  7201  caucvgprprlemloc  7206  caucvgprprlemclphr  7208  caucvgprprlemexb  7210  caucvgprprlemaddq  7211  caucvgprprlem1  7212  addcmpblnr  7229  mulcmpblnrlemg  7230  addsrmo  7233  mulsrmo  7234  addsrpr  7235  mulsrpr  7236  ltsrprg  7237  recexgt0sr  7263  mulgt0sr  7267  caucvgsrlemgt1  7284  caucvgsrlemoffval  7285  caucvgsr  7291  mulcnsr  7316  pitoregt0  7330  recidpirqlemcalc  7338  axmulcom  7350  axmulass  7352  axdistr  7353  ax0id  7357  axcnre  7360  recriota  7369  axcaucvglemcau  7377  axcaucvglemres  7378  mulid1  7429  adddirp1d  7458  mul32  7556  mul31  7557  add32  7585  add4  7587  add42  7588  cnegex  7604  addcan2  7607  addsubass  7636  subsub2  7654  nppcan2  7657  sub32  7660  nnncan  7661  sub4  7671  muladd  7806  subdi  7807  mul2neg  7820  submul2  7821  mulsub  7823  mulsubfacd  7840  add20  7896  recexre  7996  rereim  8004  apreap  8005  ltmul1  8010  cru  8020  apreim  8021  mulreim  8022  apadd1  8026  apneg  8029  mulap0  8062  divrecap  8094  divassap  8096  divmulasscomap  8102  divsubdirap  8114  divdivdivap  8119  divmul24ap  8122  divmuleqap  8123  divcanap6  8125  divdivap1  8129  divdivap2  8130  divsubdivap  8134  conjmulap  8135  div2negap  8141  apmul1  8194  cju  8356  nnmulcl  8378  add1p1  8598  sub1m1  8599  cnm2m1cnm3  8600  xp1d2m1eqxm1d2  8601  div4p1lem1div2  8602  un0addcl  8639  un0mulcl  8640  zaddcllemneg  8722  qapne  9056  cnref1o  9065  lincmb01cmp  9352  iccf1o  9353  ige3m2fz  9395  fztp  9422  fzsuc2  9423  fseq1m1p1  9439  fzm1  9444  ige2m1fz1  9453  nn0split  9475  nnsplit  9476  fzval3  9543  zpnn0elfzo1  9547  fzosplitsnm1  9548  fzosplitprm1  9573  fzoshftral  9577  rebtwn2zlemstep  9592  flhalf  9637  modqval  9659  modqvalr  9660  modqdiffl  9670  modqfrac  9672  flqmod  9673  intqfrac  9674  zmod10  9675  modqmulnn  9677  modqvalp1  9678  modqid  9684  modqcyc  9694  modqcyc2  9695  modqmul1  9712  q2submod  9720  modqdi  9727  modqsubdir  9728  modqeqmodmin  9729  modsumfzodifsn  9731  addmodlteq  9733  frecuzrdgsuctlem  9758  uzsinds  9776  iseqeq3  9784  iseqval  9788  iseqvalcbv  9789  iseqvalt  9790  iseqfclt  9794  iseqp1  9796  iseqp1t  9797  iseqm1  9801  iseqfveq2  9802  iseqshft2  9806  monoord2  9810  isermono  9811  iseqsplit  9812  iseqcaopr3  9814  iseqcaopr2  9815  iseqcaopr  9816  iseqid2  9843  iseqhomo  9844  iseqz  9845  expivallem  9854  expival  9855  expp1  9860  expnegap0  9861  expineg2  9862  expn1ap0  9863  expm1t  9881  1exp  9882  expnegzap  9887  mulexpzap  9893  expadd  9895  expaddzaplem  9896  expaddzap  9897  expmul  9898  expmulzap  9899  m1expeven  9900  expsubap  9901  expp1zap  9902  expm1ap  9903  expdivap  9904  iexpcyc  9956  subsq2  9959  binom2  9962  binom21  9963  binom2sub  9964  mulbinom2  9966  binom3  9967  zesq  9968  bernneq  9970  sqoddm1div8  10002  nn0opthlem1d  10024  nn0opthd  10026  facp1  10034  facnn2  10038  faclbnd  10045  faclbnd6  10048  bcval  10053  bccmpl  10058  bcn0  10059  bcnn  10061  bcnp1n  10063  bcm1k  10064  bcp1n  10065  bcp1nk  10066  ibcval5  10067  bcp1m1  10069  bcpasc  10070  bcn2m1  10073  bcn2p1  10074  omgadd  10106  hashunlem  10108  hashunsng  10111  hashdifsn  10123  hashxp  10130  zfz1isolemsplit  10139  zfz1isolem1  10141  zfz1iso  10142  iseqcoll  10143  shftcan1  10164  shftcan2  10165  cjval  10174  cjth  10175  crre  10186  replim  10188  remim  10189  reim0b  10191  rereb  10192  mulreap  10193  cjreb  10195  recj  10196  reneg  10197  readd  10198  resub  10199  remullem  10200  imcj  10204  imneg  10205  imadd  10206  imsub  10207  cjcj  10212  cjadd  10213  ipcnval  10215  cjmulrcl  10216  cjneg  10219  addcj  10220  cjsub  10221  cnrecnv  10239  caucvgrelemcau  10308  cvg1nlemcau  10312  cvg1nlemres  10313  recvguniqlem  10322  resqrexlemover  10338  resqrexlemlo  10341  resqrexlemcalc1  10342  resqrexlemcalc3  10344  resqrexlemnm  10346  resqrexlemcvg  10347  absneg  10378  abscj  10380  sqabsadd  10383  sqabssub  10384  absmul  10397  absid  10399  absre  10405  absresq  10406  absexpzap  10408  recvalap  10425  abstri  10432  abs2dif2  10435  recan  10437  cau3lem  10442  amgm2  10446  climaddc1  10609  climsubc1  10612  climcvg1nlem  10628  serif0  10631  isummolem3  10659  isummolem2a  10660  isummo  10662  dvdsexp  10737  oexpneg  10752  opeo  10772  omeo  10773  m1exp1  10776  flodddiv4  10809  flodddiv4t2lthalf  10812  divgcdnnr  10842  gcdaddm  10850  gcdadd  10851  gcdid  10852  modgcd  10857  bezoutlemnewy  10860  bezoutlema  10863  bezoutlemb  10864  bezoutlemex  10865  bezoutlembz  10868  absmulgcd  10881  gcdmultiple  10884  gcdmultiplez  10885  rpmulgcd  10890  rplpwr  10891  eucalginv  10913  eucialg  10916  lcmneg  10931  lcmgcdlem  10934  lcmgcd  10935  lcmid  10937  lcm1  10938  mulgcddvds  10951  qredeq  10953  divgcdcoprmex  10959  prmind2  10977  rpexp1i  11008  pw2dvdslemn  11018  pw2dvdseulemle  11020  pw2dvdseu  11021  oddpwdclemxy  11022  oddpwdclemdvds  11023  oddpwdclemndvds  11024  oddpwdclemdc  11026  2sqpwodd  11029  nn0gcdsq  11053  phiprmpw  11073  hashgcdlem  11078  qdencn  11353
  Copyright terms: Public domain W3C validator