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

Theorem oveq1d 5757
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 5749 . 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 1316  (class class class)co 5742
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 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-3an 949  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-rex 2399  df-v 2662  df-un 3045  df-sn 3503  df-pr 3504  df-op 3506  df-uni 3707  df-br 3900  df-iota 5058  df-fv 5101  df-ov 5745
This theorem is referenced by:  fvoveq1d  5764  csbov2g  5780  caovassg  5897  caovdig  5913  caovdirg  5916  caov12d  5920  caov31d  5921  caov411d  5924  grprinvlem  5933  grprinvd  5934  grpridd  5935  caofinvl  5972  omsuc  6336  nnmsucr  6352  nnm1  6388  nnm2  6389  ecovass  6506  ecoviass  6507  ecovdi  6508  ecovidi  6509  addasspig  7106  mulasspig  7108  mulpipq2  7147  distrnqg  7163  ltsonq  7174  ltanqg  7176  ltmnqg  7177  ltexnqq  7184  archnqq  7193  prarloclemarch2  7195  enq0sym  7208  addnq0mo  7223  mulnq0mo  7224  addnnnq0  7225  nqpnq0nq  7229  nq0m0r  7232  nq0a0  7233  nnanq0  7234  distrnq0  7235  addassnq0  7238  addpinq1  7240  prarloclemlo  7270  prarloclem3  7273  prarloclem5  7276  prarloclemcalc  7278  addnqprllem  7303  addnqprulem  7304  appdivnq  7339  recexprlem1ssl  7409  recexprlem1ssu  7410  ltmprr  7418  cauappcvgprlemladdru  7432  cauappcvgprlem1  7435  caucvgprlemnkj  7442  caucvgprlemnbj  7443  caucvgprlemcl  7452  caucvgprlemladdfu  7453  caucvgprlemladdrl  7454  caucvgprlem1  7455  caucvgprprlemcbv  7463  caucvgprprlemval  7464  caucvgprprlemexb  7483  caucvgprprlem1  7485  addcmpblnr  7515  mulcmpblnrlemg  7516  addsrmo  7519  mulsrmo  7520  addsrpr  7521  mulsrpr  7522  ltsrprg  7523  1idsr  7544  pn0sr  7547  recexgt0sr  7549  mulgt0sr  7554  srpospr  7559  prsradd  7562  caucvgsrlemfv  7567  caucvgsrlemcau  7569  caucvgsrlemgt1  7571  caucvgsrlemoffval  7572  caucvgsrlemoffcau  7574  caucvgsrlemoffres  7576  caucvgsrlembnd  7577  caucvgsr  7578  map2psrprg  7581  pitonnlem1p1  7622  pitonnlem2  7623  pitonn  7624  recidpirqlemcalc  7633  ax1rid  7653  axrnegex  7655  axcnre  7657  recriota  7666  nntopi  7670  axcaucvglemval  7673  axcaucvglemcau  7674  axcaucvglemres  7675  mul12  7859  mul4  7862  muladd11  7863  readdcan  7870  muladd11r  7886  add12  7888  cnegex  7908  addcan  7910  negeu  7921  pncan2  7937  addsubass  7940  addsub  7941  2addsub  7944  addsubeq4  7945  subid  7949  subid1  7950  npncan  7951  nppcan  7952  nnpcan  7953  nnncan1  7966  npncan3  7968  pnpcan  7969  pnncan  7971  ppncan  7972  addsub4  7973  negsub  7978  subneg  7979  subeqxfrd  8093  mvlraddd  8094  mvlladdd  8095  mvrraddd  8096  subaddeqd  8099  ine0  8124  mulneg1  8125  ltadd2  8149  apreap  8316  cru  8331  recexap  8381  mulcanapd  8389  div23ap  8418  div13ap  8420  divmulassap  8422  divmulasscomap  8423  divcanap4  8426  muldivdirap  8434  divsubdirap  8435  divmuldivap  8439  divdivdivap  8440  divcanap5  8441  divmul13ap  8442  divmuleqap  8444  divdiv32ap  8447  divcanap7  8448  dmdcanap  8449  divdivap1  8450  divdivap2  8451  divadddivap  8454  divsubdivap  8455  conjmulap  8456  divneg2ap  8463  mvllmulapd  8565  lt2mul2div  8601  nndivtr  8726  2halves  8907  halfaddsub  8912  avgle1  8918  avgle2  8919  div4p1lem1div2  8931  un0addcl  8968  un0mulcl  8969  peano2z  9048  zneo  9110  nneoor  9111  nneo  9112  zeo  9114  zeo2  9115  deceq1  9144  qreccl  9390  xaddcom  9599  xnegdi  9606  xaddass  9607  xaddass2  9608  xpncan  9609  xleadd1a  9611  xltadd1  9614  xposdif  9620  xadd4d  9623  lincmb01cmp  9741  iccf1o  9742  fzosubel3  9928  qavgle  9991  2tnp1ge0ge0  10029  fldiv4p1lem1div2  10033  ceilqm1lt  10040  flqdiv  10049  modqlt  10061  modqdiffl  10063  modqcyc2  10088  modqaddabs  10090  mulqaddmodid  10092  mulp1mod1  10093  modqmuladd  10094  modqmuladdnn0  10096  qnegmod  10097  addmodid  10100  addmodidr  10101  modqadd2mod  10102  modqm1p1mod0  10103  modqmul12d  10106  modqnegd  10107  modqadd12d  10108  modqsub12d  10109  q2submod  10113  modqmulmodr  10118  modqaddmulmod  10119  modqsubdir  10121  modfzo0difsn  10123  modsumfzodifsn  10124  addmodlteq  10126  frecuzrdgsuc  10142  frecfzennn  10154  iseqovex  10184  seq3-1p  10208  seq3caopr2  10210  seq3caopr  10211  seq3id  10236  seq3homo  10238  seq3z  10239  expp1  10255  exprecap  10289  expaddzaplem  10291  expmulzap  10294  expdivap  10299  sqval  10306  sqsubswap  10308  subsq  10354  subsq2  10355  binom2  10358  binom2sub  10360  mulbinom2  10363  binom3  10364  zesq  10365  bernneq2  10368  sqoddm1div8  10399  nn0opthlem1d  10421  nn0opthd  10423  nn0opth2d  10424  facp1  10431  facdiv  10439  facndiv  10440  faclbnd  10442  faclbnd2  10443  faclbnd3  10444  bcval  10450  bccmpl  10455  bcm1k  10461  bcp1n  10462  bcp1nk  10463  bcval5  10464  bcp1m1  10466  bcpasc  10467  bcn2m1  10470  hashprg  10509  hashdifpr  10521  hashfzo  10523  hashfzp1  10525  hashfz0  10526  hashxp  10527  zfz1isolemsplit  10536  zfz1isolem1  10538  seq3coll  10540  reval  10576  crre  10584  remim  10587  remul2  10600  immul2  10607  imval2  10621  cjdivap  10636  caucvgre  10708  cvg1nlemcau  10711  cvg1nlemres  10712  resqrexlemp1rp  10733  resqrexlemfp1  10736  resqrexlemover  10737  resqrexlemcalc1  10741  resqrexlemcalc3  10743  resqrexlemnm  10745  resqrexlemoverl  10748  resqrexlemglsq  10749  resqrexlemga  10750  resqrexlemsqa  10751  resqrexlemex  10752  resqrex  10753  sqrtdiv  10769  absvalsq  10780  absreimsq  10794  absdivap  10797  cau3lem  10841  maxabslemlub  10934  maxabslemval  10935  max0addsup  10946  minabs  10962  bdtrilem  10965  bdtri  10966  xrmaxaddlem  10984  xrmaxadd  10985  xrbdtri  11000  clim  11005  clim2  11007  climshftlemg  11026  climshft2  11030  climcn1  11032  climcn2  11033  subcn2  11035  reccn2ap  11037  climmulc2  11055  climsubc2  11057  clim2ser  11061  iser3shft  11070  climcau  11071  serf0  11076  fzosump1  11141  fsum1p  11142  fsump1  11144  sumsplitdc  11156  fsump1i  11157  mptfzshft  11166  fisum0diag2  11171  fsumconst  11178  fsumdifsnconst  11179  modfsummodlemstep  11181  modfsummod  11182  telfsumo  11190  fsumparts  11194  fsumrelem  11195  hash2iun1dif1  11204  binomlem  11207  binom  11208  binom1p  11209  binom1dif  11211  bcxmas  11213  isumsplit  11215  isum1p  11216  arisum  11222  arisum2  11223  trireciplem  11224  geoserap  11231  geolim  11235  geolim2  11236  georeclim  11237  geo2sum  11238  geoisum1  11243  cvgratnnlemseq  11250  cvgratnnlemsumlt  11252  cvgratnnlemfm  11253  cvgratz  11256  mertenslemi1  11259  mertenslem2  11260  mertensabs  11261  efcllemp  11278  ef0lem  11280  efval  11281  esum  11282  ege2le3  11291  efaddlem  11294  efsep  11311  effsumlt  11312  eft0val  11313  efgt1p2  11315  efgt1p  11316  sinval  11323  cosval  11324  resinval  11336  recosval  11337  efi4p  11338  resin4p  11339  recos4p  11340  sinneg  11347  cosneg  11348  efival  11353  sinadd  11357  cosadd  11358  tanaddap  11360  sinmul  11365  cosmul  11366  cos2t  11371  cos2tsin  11372  ef01bndlem  11377  absefib  11391  demoivre  11393  demoivreALT  11394  eirraplem  11395  moddvds  11414  mulmoddvds  11473  3dvds2dec  11475  zeo3  11477  odd2np1lem  11481  odd2np1  11482  oexpneg  11486  2tp1odd  11493  ltoddhalfle  11502  opoe  11504  opeo  11506  omeo  11507  m1expo  11509  m1exp1  11510  nn0o1gt2  11514  nn0o  11516  divalglemnn  11527  divalglemqt  11528  divalglemeunn  11530  divalglemex  11531  divalglemeuneg  11532  flodddiv4  11543  flodddiv4t2lthalf  11546  gcdaddm  11584  bezoutlemnewy  11596  bezoutlema  11599  bezoutlemb  11600  bezoutlemex  11601  bezoutlemaz  11603  mulgcd  11616  gcddiv  11619  gcdmultiplez  11621  rpmulgcd  11626  rplpwr  11627  lcmgcdlem  11670  lcmgcd  11671  divgcdcoprmex  11695  cncongr2  11697  prmexpb  11741  rpexp  11743  rpexp1i  11744  sqrt2irrlem  11751  oddpwdclemxy  11758  oddpwdclemndvds  11760  sqpweven  11764  2sqpwodd  11765  sqne2sq  11766  qmuldeneqnum  11784  nn0gcdsq  11789  zgcdsq  11790  numdensq  11791  dfphi2  11807  phiprmpw  11809  phiprm  11810  hashgcdlem  11814  ennnfonelemkh  11836  ennnfonelemhf1o  11837  resttop  12250  restco  12254  restin  12256  lmfval  12272  cnprcl2k  12286  txrest  12356  txdis1cn  12358  cnmpt2res  12377  psmettri2  12408  psmettri  12410  xmettri2  12441  xmettri  12452  mettri  12453  metrtri  12457  blvalps  12468  blval  12469  xblss2  12485  blhalf  12488  comet  12579  xmetxp  12587  txmetcnp  12598  cnmet  12610  ioo2bl  12623  limcmpted  12712  limcimolemlt  12713  cnplimclemr  12718  limccnp2cntop  12726  reldvg  12728  dvfvalap  12730  dvidlemap  12740  dvconst  12741  dvcnp2cntop  12743  dvaddxxbr  12745  dvmulxxbr  12746  dvcoapbr  12751  dvcjbr  12752  dvexp  12755  dvrecap  12757  dvmptcmulcn  12763  dveflem  12766  sin0pilem1  12773  sinperlem  12800  ptolemy  12816  trilpolemeq1  13129  trilpolemlt1  13130
  Copyright terms: Public domain W3C validator