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

Theorem oveq1d 5883
Description: Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.)
Hypothesis
Ref Expression
oveq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
oveq1d  |-  ( ph  ->  ( A F C )  =  ( B F C ) )

Proof of Theorem oveq1d
StepHypRef Expression
1 oveq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 oveq1 5875 . 2  |-  ( A  =  B  ->  ( A F C )  =  ( B F C ) )
31, 2syl 14 1  |-  ( ph  ->  ( A F C )  =  ( B F C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1353  (class class class)co 5868
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2739  df-un 3133  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-br 4001  df-iota 5173  df-fv 5219  df-ov 5871
This theorem is referenced by:  fvoveq1d  5890  csbov2g  5909  caovassg  6026  caovdig  6042  caovdirg  6045  caov12d  6049  caov31d  6050  caov411d  6053  caofinvl  6098  omsuc  6466  nnmsucr  6482  nnm1  6519  nnm2  6520  ecovass  6637  ecoviass  6638  ecovdi  6639  ecovidi  6640  addasspig  7307  mulasspig  7309  mulpipq2  7348  distrnqg  7364  ltsonq  7375  ltanqg  7377  ltmnqg  7378  ltexnqq  7385  archnqq  7394  prarloclemarch2  7396  enq0sym  7409  addnq0mo  7424  mulnq0mo  7425  addnnnq0  7426  nqpnq0nq  7430  nq0m0r  7433  nq0a0  7434  nnanq0  7435  distrnq0  7436  addassnq0  7439  addpinq1  7441  prarloclemlo  7471  prarloclem3  7474  prarloclem5  7477  prarloclemcalc  7479  addnqprllem  7504  addnqprulem  7505  appdivnq  7540  recexprlem1ssl  7610  recexprlem1ssu  7611  ltmprr  7619  cauappcvgprlemladdru  7633  cauappcvgprlem1  7636  caucvgprlemnkj  7643  caucvgprlemnbj  7644  caucvgprlemcl  7653  caucvgprlemladdfu  7654  caucvgprlemladdrl  7655  caucvgprlem1  7656  caucvgprprlemcbv  7664  caucvgprprlemval  7665  caucvgprprlemexb  7684  caucvgprprlem1  7686  addcmpblnr  7716  mulcmpblnrlemg  7717  addsrmo  7720  mulsrmo  7721  addsrpr  7722  mulsrpr  7723  ltsrprg  7724  1idsr  7745  pn0sr  7748  recexgt0sr  7750  mulgt0sr  7755  srpospr  7760  prsradd  7763  caucvgsrlemfv  7768  caucvgsrlemcau  7770  caucvgsrlemgt1  7772  caucvgsrlemoffval  7773  caucvgsrlemoffcau  7775  caucvgsrlemoffres  7777  caucvgsrlembnd  7778  caucvgsr  7779  map2psrprg  7782  pitonnlem1p1  7823  pitonnlem2  7824  pitonn  7825  recidpirqlemcalc  7834  ax1rid  7854  axrnegex  7856  axcnre  7858  recriota  7867  nntopi  7871  axcaucvglemval  7874  axcaucvglemcau  7875  axcaucvglemres  7876  mul12  8063  mul4  8066  muladd11  8067  readdcan  8074  muladd11r  8090  add12  8092  cnegex  8112  addcan  8114  negeu  8125  pncan2  8141  addsubass  8144  addsub  8145  2addsub  8148  addsubeq4  8149  subid  8153  subid1  8154  npncan  8155  nppcan  8156  nnpcan  8157  nnncan1  8170  npncan3  8172  pnpcan  8173  pnncan  8175  ppncan  8176  addsub4  8177  negsub  8182  subneg  8183  subeqxfrd  8297  mvlraddd  8298  mvlladdd  8299  mvrraddd  8300  subaddeqd  8303  ine0  8328  mulneg1  8329  ltadd2  8353  apreap  8521  cru  8536  recexap  8586  mulcanapd  8594  div23ap  8624  div13ap  8626  divmulassap  8628  divmulasscomap  8629  divcanap4  8632  muldivdirap  8640  divsubdirap  8641  divmuldivap  8645  divdivdivap  8646  divcanap5  8647  divmul13ap  8648  divmuleqap  8650  divdiv32ap  8653  divcanap7  8654  dmdcanap  8655  divdivap1  8656  divdivap2  8657  divadddivap  8660  divsubdivap  8661  conjmulap  8662  divneg2ap  8669  subrecap  8772  mvllmulapd  8775  lt2mul2div  8812  nndivtr  8937  2halves  9124  halfaddsub  9129  avgle1  9135  avgle2  9136  div4p1lem1div2  9148  un0addcl  9185  un0mulcl  9186  peano2z  9265  zneo  9330  nneoor  9331  nneo  9332  zeo  9334  zeo2  9335  deceq1  9364  qreccl  9618  xaddcom  9835  xnegdi  9842  xaddass  9843  xaddass2  9844  xpncan  9845  xleadd1a  9847  xltadd1  9850  xposdif  9856  xadd4d  9859  lincmb01cmp  9977  iccf1o  9978  fz0to4untppr  10097  fzosubel3  10169  qavgle  10232  2tnp1ge0ge0  10274  fldiv4p1lem1div2  10278  ceilqm1lt  10285  flqdiv  10294  modqlt  10306  modqdiffl  10308  modqcyc2  10333  modqaddabs  10335  mulqaddmodid  10337  mulp1mod1  10338  modqmuladd  10339  modqmuladdnn0  10341  qnegmod  10342  addmodid  10345  addmodidr  10346  modqadd2mod  10347  modqm1p1mod0  10348  modqmul12d  10351  modqnegd  10352  modqadd12d  10353  modqsub12d  10354  q2submod  10358  modqmulmodr  10363  modqaddmulmod  10364  modqsubdir  10366  modfzo0difsn  10368  modsumfzodifsn  10369  addmodlteq  10371  frecuzrdgsuc  10387  frecfzennn  10399  iseqovex  10429  seq3-1p  10453  seq3caopr2  10455  seq3caopr  10456  seq3id  10481  seq3homo  10483  seq3z  10484  expp1  10500  exprecap  10534  expaddzaplem  10536  expmulzap  10539  expdivap  10544  sqval  10551  sqsubswap  10553  subsq  10599  subsq2  10600  binom2  10604  binom2sub  10606  mulbinom2  10609  binom3  10610  zesq  10611  bernneq2  10614  modqexp  10619  sqoddm1div8  10646  nn0opthlem1d  10671  nn0opthd  10673  nn0opth2d  10674  facp1  10681  facdiv  10689  facndiv  10690  faclbnd  10692  faclbnd2  10693  faclbnd3  10694  bcval  10700  bccmpl  10705  bcm1k  10711  bcp1n  10712  bcp1nk  10713  bcval5  10714  bcp1m1  10716  bcpasc  10717  bcn2m1  10720  hashprg  10759  hashdifpr  10771  hashfzo  10773  hashfzp1  10775  hashfz0  10776  hashxp  10777  zfz1isolemsplit  10789  zfz1isolem1  10791  seq3coll  10793  reval  10829  crre  10837  remim  10840  remul2  10853  immul2  10860  imval2  10874  cjdivap  10889  caucvgre  10961  cvg1nlemcau  10964  cvg1nlemres  10965  resqrexlemp1rp  10986  resqrexlemfp1  10989  resqrexlemover  10990  resqrexlemcalc1  10994  resqrexlemcalc3  10996  resqrexlemnm  10998  resqrexlemoverl  11001  resqrexlemglsq  11002  resqrexlemga  11003  resqrexlemsqa  11004  resqrexlemex  11005  resqrex  11006  sqrtdiv  11022  absvalsq  11033  absreimsq  11047  absdivap  11050  cau3lem  11094  maxabslemlub  11187  maxabslemval  11188  max0addsup  11199  minabs  11215  bdtrilem  11218  bdtri  11219  xrmaxaddlem  11239  xrmaxadd  11240  xrbdtri  11255  clim  11260  clim2  11262  climshftlemg  11281  climshft2  11285  climcn1  11287  climcn2  11288  subcn2  11290  reccn2ap  11292  climmulc2  11310  climsubc2  11312  clim2ser  11316  iser3shft  11325  climcau  11326  serf0  11331  fzosump1  11396  fsum1p  11397  fsump1  11399  sumsplitdc  11411  fsump1i  11412  mptfzshft  11421  fisum0diag2  11426  fsumconst  11433  fsumdifsnconst  11434  modfsummodlemstep  11436  modfsummod  11437  telfsumo  11445  fsumparts  11449  fsumrelem  11450  hash2iun1dif1  11459  binomlem  11462  binom  11463  binom1p  11464  binom1dif  11466  bcxmas  11468  isumsplit  11470  isum1p  11471  arisum  11477  arisum2  11478  trireciplem  11479  geoserap  11486  geolim  11490  geolim2  11491  georeclim  11492  geo2sum  11493  geoisum1  11498  cvgratnnlemseq  11505  cvgratnnlemsumlt  11507  cvgratnnlemfm  11508  cvgratz  11511  mertenslemi1  11514  mertenslem2  11515  mertensabs  11516  fprod1p  11578  fprodp1  11579  fprodcl2lem  11584  fprodfac  11594  fprodeq0  11596  fprodconst  11599  fprodrec  11608  fprodsplit1f  11613  fprodmodd  11620  efcllemp  11637  ef0lem  11639  efval  11640  esum  11641  ege2le3  11650  efaddlem  11653  efsep  11670  effsumlt  11671  eft0val  11672  efgt1p2  11674  efgt1p  11675  sinval  11681  cosval  11682  resinval  11694  recosval  11695  efi4p  11696  resin4p  11697  recos4p  11698  sinneg  11705  cosneg  11706  efival  11711  sinadd  11715  cosadd  11716  tanaddap  11718  sinmul  11723  cosmul  11724  cos2t  11729  cos2tsin  11730  ef01bndlem  11735  absefib  11749  demoivre  11751  demoivreALT  11752  eirraplem  11755  p1modz1  11772  dvdsmodexp  11773  moddvds  11777  mulmoddvds  11839  3dvds2dec  11841  zeo3  11843  odd2np1lem  11847  odd2np1  11848  oexpneg  11852  2tp1odd  11859  ltoddhalfle  11868  opoe  11870  opeo  11872  omeo  11873  m1expo  11875  m1exp1  11876  nn0o1gt2  11880  nn0o  11882  divalglemnn  11893  divalglemqt  11894  divalglemeunn  11896  divalglemex  11897  divalglemeuneg  11898  flodddiv4  11909  flodddiv4t2lthalf  11912  gcdaddm  11955  bezoutlemnewy  11967  bezoutlema  11970  bezoutlemb  11971  bezoutlemex  11972  bezoutlemaz  11974  mulgcd  11987  gcddiv  11990  gcdmultiplez  11992  rpmulgcd  11997  rplpwr  11998  uzwodc  12008  lcmgcdlem  12047  lcmgcd  12048  divgcdcoprmex  12072  cncongr2  12074  prmexpb  12121  rpexp  12123  rpexp1i  12124  sqrt2irrlem  12131  oddpwdclemxy  12139  oddpwdclemndvds  12141  sqpweven  12145  2sqpwodd  12146  sqne2sq  12147  qmuldeneqnum  12165  nn0gcdsq  12170  zgcdsq  12171  numdensq  12172  dfphi2  12190  phiprmpw  12192  phiprm  12193  eulerthlema  12200  eulerthlemh  12201  eulerthlemth  12202  fermltl  12204  prmdiv  12205  prmdiveq  12206  prmdivdiv  12207  hashgcdlem  12208  odzval  12211  odzcllem  12212  odzdvds  12215  vfermltl  12221  powm2modprm  12222  reumodprminv  12223  modprm0  12224  nnnn0modprm0  12225  modprmn0modprm0  12226  coprimeprodsq  12227  coprimeprodsq2  12228  pythagtriplem1  12235  pythagtriplem3  12237  pythagtriplem4  12238  pythagtriplem6  12240  pythagtriplem7  12241  pythagtriplem12  12245  pythagtriplem14  12247  pythagtriplem15  12248  pythagtriplem16  12249  pythagtriplem17  12250  pythagtriplem18  12251  pceu  12265  pczpre  12267  pcdiv  12272  pcqdiv  12277  pcrec  12278  pczndvds  12285  pcneg  12294  pc2dvds  12299  pcprmpw2  12302  pcaddlem  12308  pcadd  12309  fldivp1  12316  pockthlem  12324  pockthi  12326  4sqlem5  12350  4sqlem9  12354  4sqlem10  12355  4sqlem2  12357  4sqlem3  12358  4sqlem4  12360  mul4sqlem  12361  ennnfonelemkh  12383  ennnfonelemhf1o  12384  ressressg  12503  grprinvlem  12683  grprinvd  12684  grpridd  12685  isnsgrp  12691  sgrpass  12693  sgrp1  12695  mnd12g  12708  mndpropd  12720  mhmlin  12735  grprcan  12787  grpinvid1  12801  isgrpinv  12803  grplcan  12808  grpasscan1  12809  grplmulf1o  12820  grpinvadd  12824  grpinvsub  12828  grpsubsub4  12839  grppnpcan2  12840  grpnpncan  12841  dfgrp3mlem  12844  dfgrp3m  12845  grplactcnv  12848  mhmlem  12854  mhmid  12855  mhmmnd  12856  mulgnnp1  12867  mulg2  12868  mulgnn0p1  12870  mulgsubcl  12873  mulgneg  12877  mulgaddcomlem  12881  mulgaddcom  12882  mulgz  12886  mulgnn0dir  12888  mulgdirlem  12889  mulgdir  12890  mulgneg2  12892  mulgnnass  12893  mulgnn0ass  12894  mulgass  12895  mulgassr  12896  mulgmodid  12897  mulgsubdir  12898  ablsub2inv  12928  abladdsub4  12931  abladdsub  12932  ablpncan2  12933  ablpnpcan  12937  ablnncan  12938  ablnnncan1  12941  srgass  12967  srgmulgass  12985  srgpcomp  12986  srgpcompp  12987  srgpcomppsc  12988  ringpropd  13030  ringlz  13035  ring1eq0  13038  ringnegl  13041  ringmneg1  13043  rngsubdir  13047  mulgass2  13048  ring1  13049  opprring  13061  unitgrp  13097  resttop  13303  restco  13307  restin  13309  lmfval  13325  cnprcl2k  13339  txrest  13409  txdis1cn  13411  cnmpt2res  13430  psmettri2  13461  psmettri  13463  xmettri2  13494  xmettri  13505  mettri  13506  metrtri  13510  blvalps  13521  blval  13522  xblss2  13538  blhalf  13541  comet  13632  xmetxp  13640  txmetcnp  13651  cnmet  13663  ioo2bl  13676  limcmpted  13765  limcimolemlt  13766  cnplimclemr  13771  limccnp2cntop  13779  reldvg  13781  dvfvalap  13783  dvidlemap  13793  dvconst  13794  dvcnp2cntop  13796  dvaddxxbr  13798  dvmulxxbr  13799  dvcoapbr  13804  dvcjbr  13805  dvexp  13808  dvrecap  13810  dvmptcmulcn  13816  dveflem  13820  sin0pilem1  13835  sinperlem  13862  ptolemy  13878  tangtx  13892  abssinper  13900  reexplog  13925  relogexp  13926  cxprec  13964  rpdivcxp  13965  cxpmul  13966  rpabscxpbnd  13992  rplogbval  13996  rplogbreexp  14004  rprelogbmul  14006  logbrec  14011  logbgcd1irraplemap  14020  binom4  14030  lgslem1  14034  lgslem4  14037  lgsval  14038  lgsfvalg  14039  lgsval2lem  14044  lgsval4lem  14045  lgsvalmod  14053  lgsneg  14058  lgsneg1  14059  lgsmod  14060  lgsdilem  14061  lgsdir2lem4  14065  lgsdir2  14067  lgsdirprm  14068  lgsdir  14069  lgsne0  14072  lgssq  14074  lgssq2  14075  lgsmulsqcoprm  14080  lgsdirnn0  14081  lgsdinn0  14082  2sqlem1  14083  2sqlem2  14084  mul2sq  14085  2sqlem3  14086  2sqlem4  14087  2sqlem8  14092  2sqlem9  14093  2sqlem10  14094  trilpolemeq1  14411  trilpolemlt1  14412  trirec0xor  14416  apdifflemf  14417  apdiff  14419
  Copyright terms: Public domain W3C validator