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

Theorem oveq1d 5755
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 5747 . 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 1314  (class class class)co 5740
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-rex 2397  df-v 2660  df-un 3043  df-sn 3501  df-pr 3502  df-op 3504  df-uni 3705  df-br 3898  df-iota 5056  df-fv 5099  df-ov 5743
This theorem is referenced by:  fvoveq1d  5762  csbov2g  5778  caovassg  5895  caovdig  5911  caovdirg  5914  caov12d  5918  caov31d  5919  caov411d  5922  grprinvlem  5931  grprinvd  5932  grpridd  5933  caofinvl  5970  omsuc  6334  nnmsucr  6350  nnm1  6386  nnm2  6387  ecovass  6504  ecoviass  6505  ecovdi  6506  ecovidi  6507  addasspig  7102  mulasspig  7104  mulpipq2  7143  distrnqg  7159  ltsonq  7170  ltanqg  7172  ltmnqg  7173  ltexnqq  7180  archnqq  7189  prarloclemarch2  7191  enq0sym  7204  addnq0mo  7219  mulnq0mo  7220  addnnnq0  7221  nqpnq0nq  7225  nq0m0r  7228  nq0a0  7229  nnanq0  7230  distrnq0  7231  addassnq0  7234  addpinq1  7236  prarloclemlo  7266  prarloclem3  7269  prarloclem5  7272  prarloclemcalc  7274  addnqprllem  7299  addnqprulem  7300  appdivnq  7335  recexprlem1ssl  7405  recexprlem1ssu  7406  ltmprr  7414  cauappcvgprlemladdru  7428  cauappcvgprlem1  7431  caucvgprlemnkj  7438  caucvgprlemnbj  7439  caucvgprlemcl  7448  caucvgprlemladdfu  7449  caucvgprlemladdrl  7450  caucvgprlem1  7451  caucvgprprlemcbv  7459  caucvgprprlemval  7460  caucvgprprlemexb  7479  caucvgprprlem1  7481  addcmpblnr  7511  mulcmpblnrlemg  7512  addsrmo  7515  mulsrmo  7516  addsrpr  7517  mulsrpr  7518  ltsrprg  7519  1idsr  7540  pn0sr  7543  recexgt0sr  7545  mulgt0sr  7550  srpospr  7555  prsradd  7558  caucvgsrlemfv  7563  caucvgsrlemcau  7565  caucvgsrlemgt1  7567  caucvgsrlemoffval  7568  caucvgsrlemoffcau  7570  caucvgsrlemoffres  7572  caucvgsrlembnd  7573  caucvgsr  7574  map2psrprg  7577  pitonnlem1p1  7618  pitonnlem2  7619  pitonn  7620  recidpirqlemcalc  7629  ax1rid  7649  axrnegex  7651  axcnre  7653  recriota  7662  nntopi  7666  axcaucvglemval  7669  axcaucvglemcau  7670  axcaucvglemres  7671  mul12  7855  mul4  7858  muladd11  7859  readdcan  7866  muladd11r  7882  add12  7884  cnegex  7904  addcan  7906  negeu  7917  pncan2  7933  addsubass  7936  addsub  7937  2addsub  7940  addsubeq4  7941  subid  7945  subid1  7946  npncan  7947  nppcan  7948  nnpcan  7949  nnncan1  7962  npncan3  7964  pnpcan  7965  pnncan  7967  ppncan  7968  addsub4  7969  negsub  7974  subneg  7975  subeqxfrd  8089  mvlraddd  8090  mvlladdd  8091  mvrraddd  8092  subaddeqd  8095  ine0  8120  mulneg1  8121  ltadd2  8145  apreap  8312  cru  8327  recexap  8374  mulcanapd  8382  div23ap  8411  div13ap  8413  divmulassap  8415  divmulasscomap  8416  divcanap4  8419  muldivdirap  8427  divsubdirap  8428  divmuldivap  8432  divdivdivap  8433  divcanap5  8434  divmul13ap  8435  divmuleqap  8437  divdiv32ap  8440  divcanap7  8441  dmdcanap  8442  divdivap1  8443  divdivap2  8444  divadddivap  8447  divsubdivap  8448  conjmulap  8449  divneg2ap  8456  mvllmulapd  8558  lt2mul2div  8594  nndivtr  8719  2halves  8900  halfaddsub  8905  avgle1  8911  avgle2  8912  div4p1lem1div2  8924  un0addcl  8961  un0mulcl  8962  peano2z  9041  zneo  9103  nneoor  9104  nneo  9105  zeo  9107  zeo2  9108  deceq1  9137  qreccl  9383  xaddcom  9584  xnegdi  9591  xaddass  9592  xaddass2  9593  xpncan  9594  xleadd1a  9596  xltadd1  9599  xposdif  9605  xadd4d  9608  lincmb01cmp  9726  iccf1o  9727  fzosubel3  9913  qavgle  9976  2tnp1ge0ge0  10014  fldiv4p1lem1div2  10018  ceilqm1lt  10025  flqdiv  10034  modqlt  10046  modqdiffl  10048  modqcyc2  10073  modqaddabs  10075  mulqaddmodid  10077  mulp1mod1  10078  modqmuladd  10079  modqmuladdnn0  10081  qnegmod  10082  addmodid  10085  addmodidr  10086  modqadd2mod  10087  modqm1p1mod0  10088  modqmul12d  10091  modqnegd  10092  modqadd12d  10093  modqsub12d  10094  q2submod  10098  modqmulmodr  10103  modqaddmulmod  10104  modqsubdir  10106  modfzo0difsn  10108  modsumfzodifsn  10109  addmodlteq  10111  frecuzrdgsuc  10127  frecfzennn  10139  iseqovex  10169  seq3-1p  10193  seq3caopr2  10195  seq3caopr  10196  seq3id  10221  seq3homo  10223  seq3z  10224  expp1  10240  exprecap  10274  expaddzaplem  10276  expmulzap  10279  expdivap  10284  sqval  10291  sqsubswap  10293  subsq  10339  subsq2  10340  binom2  10343  binom2sub  10345  mulbinom2  10348  binom3  10349  zesq  10350  bernneq2  10353  sqoddm1div8  10384  nn0opthlem1d  10406  nn0opthd  10408  nn0opth2d  10409  facp1  10416  facdiv  10424  facndiv  10425  faclbnd  10427  faclbnd2  10428  faclbnd3  10429  bcval  10435  bccmpl  10440  bcm1k  10446  bcp1n  10447  bcp1nk  10448  bcval5  10449  bcp1m1  10451  bcpasc  10452  bcn2m1  10455  hashprg  10494  hashdifpr  10506  hashfzo  10508  hashfzp1  10510  hashfz0  10511  hashxp  10512  zfz1isolemsplit  10521  zfz1isolem1  10523  seq3coll  10525  reval  10561  crre  10569  remim  10572  remul2  10585  immul2  10592  imval2  10606  cjdivap  10621  caucvgre  10693  cvg1nlemcau  10696  cvg1nlemres  10697  resqrexlemp1rp  10718  resqrexlemfp1  10721  resqrexlemover  10722  resqrexlemcalc1  10726  resqrexlemcalc3  10728  resqrexlemnm  10730  resqrexlemoverl  10733  resqrexlemglsq  10734  resqrexlemga  10735  resqrexlemsqa  10736  resqrexlemex  10737  resqrex  10738  sqrtdiv  10754  absvalsq  10765  absreimsq  10779  absdivap  10782  cau3lem  10826  maxabslemlub  10919  maxabslemval  10920  max0addsup  10931  minabs  10947  bdtrilem  10950  bdtri  10951  xrmaxaddlem  10969  xrmaxadd  10970  xrbdtri  10985  clim  10990  clim2  10992  climshftlemg  11011  climshft2  11015  climcn1  11017  climcn2  11018  subcn2  11020  reccn2ap  11022  climmulc2  11040  climsubc2  11042  clim2ser  11046  iser3shft  11055  climcau  11056  serf0  11061  fzosump1  11126  fsum1p  11127  fsump1  11129  sumsplitdc  11141  fsump1i  11142  mptfzshft  11151  fisum0diag2  11156  fsumconst  11163  fsumdifsnconst  11164  modfsummodlemstep  11166  modfsummod  11167  telfsumo  11175  fsumparts  11179  fsumrelem  11180  hash2iun1dif1  11189  binomlem  11192  binom  11193  binom1p  11194  binom1dif  11196  bcxmas  11198  isumsplit  11200  isum1p  11201  arisum  11207  arisum2  11208  trireciplem  11209  geoserap  11216  geolim  11220  geolim2  11221  georeclim  11222  geo2sum  11223  geoisum1  11228  cvgratnnlemseq  11235  cvgratnnlemsumlt  11237  cvgratnnlemfm  11238  cvgratz  11241  mertenslemi1  11244  mertenslem2  11245  mertensabs  11246  efcllemp  11263  ef0lem  11265  efval  11266  esum  11267  ege2le3  11276  efaddlem  11279  efsep  11296  effsumlt  11297  eft0val  11298  efgt1p2  11300  efgt1p  11301  sinval  11308  cosval  11309  resinval  11321  recosval  11322  efi4p  11323  resin4p  11324  recos4p  11325  sinneg  11332  cosneg  11333  efival  11338  sinadd  11342  cosadd  11343  tanaddap  11345  sinmul  11350  cosmul  11351  cos2t  11356  cos2tsin  11357  ef01bndlem  11362  absefib  11375  demoivre  11377  demoivreALT  11378  eirraplem  11379  moddvds  11398  mulmoddvds  11457  3dvds2dec  11459  zeo3  11461  odd2np1lem  11465  odd2np1  11466  oexpneg  11470  2tp1odd  11477  ltoddhalfle  11486  opoe  11488  opeo  11490  omeo  11491  m1expo  11493  m1exp1  11494  nn0o1gt2  11498  nn0o  11500  divalglemnn  11511  divalglemqt  11512  divalglemeunn  11514  divalglemex  11515  divalglemeuneg  11516  flodddiv4  11527  flodddiv4t2lthalf  11530  gcdaddm  11568  bezoutlemnewy  11580  bezoutlema  11583  bezoutlemb  11584  bezoutlemex  11585  bezoutlemaz  11587  mulgcd  11600  gcddiv  11603  gcdmultiplez  11605  rpmulgcd  11610  rplpwr  11611  lcmgcdlem  11654  lcmgcd  11655  divgcdcoprmex  11679  cncongr2  11681  prmexpb  11725  rpexp  11727  rpexp1i  11728  sqrt2irrlem  11735  oddpwdclemxy  11742  oddpwdclemndvds  11744  sqpweven  11748  2sqpwodd  11749  sqne2sq  11750  qmuldeneqnum  11768  nn0gcdsq  11773  zgcdsq  11774  numdensq  11775  dfphi2  11791  phiprmpw  11793  phiprm  11794  hashgcdlem  11798  ennnfonelemkh  11820  ennnfonelemhf1o  11821  resttop  12234  restco  12238  restin  12240  lmfval  12256  cnprcl2k  12270  txrest  12340  txdis1cn  12342  cnmpt2res  12361  psmettri2  12392  psmettri  12394  xmettri2  12425  xmettri  12436  mettri  12437  metrtri  12441  blvalps  12452  blval  12453  xblss2  12469  blhalf  12472  comet  12563  xmetxp  12571  txmetcnp  12582  cnmet  12594  ioo2bl  12607  limcmpted  12684  limcimolemlt  12685  cnplimclemr  12690  limccnp2cntop  12698  reldvg  12700  dvfvalap  12702  dvidlemap  12712  dvconst  12713  dvcnp2cntop  12715  dvaddxxbr  12717  dvmulxxbr  12718  dvcoapbr  12723  dvcjbr  12724  dvexp  12727  dvrecap  12729  dvmptcmulcn  12735  dveflem  12738  trilpolemeq1  13044  trilpolemlt1  13045
  Copyright terms: Public domain W3C validator