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

Theorem oveq1d 5554
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 5546 . 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 1259  (class class class)co 5539
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-3an 898  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-rex 2329  df-v 2576  df-un 2949  df-sn 3408  df-pr 3409  df-op 3411  df-uni 3608  df-br 3792  df-iota 4894  df-fv 4937  df-ov 5542
This theorem is referenced by:  csbov2g  5573  caovassg  5686  caovdig  5702  caovdirg  5705  caov12d  5709  caov31d  5710  caov411d  5713  grprinvlem  5722  grprinvd  5723  grpridd  5724  caofinvl  5760  omsuc  6081  nnmsucr  6097  nnm1  6127  nnm2  6128  ecovass  6245  ecoviass  6246  ecovdi  6247  ecovidi  6248  addasspig  6485  mulasspig  6487  mulpipq2  6526  distrnqg  6542  ltsonq  6553  ltanqg  6555  ltmnqg  6556  ltexnqq  6563  archnqq  6572  prarloclemarch2  6574  enq0sym  6587  addnq0mo  6602  mulnq0mo  6603  addnnnq0  6604  nqpnq0nq  6608  nq0m0r  6611  nq0a0  6612  nnanq0  6613  distrnq0  6614  addassnq0  6617  addpinq1  6619  prarloclemlo  6649  prarloclem3  6652  prarloclem5  6655  prarloclemcalc  6657  addnqprllem  6682  addnqprulem  6683  appdivnq  6718  recexprlem1ssl  6788  recexprlem1ssu  6789  ltmprr  6797  cauappcvgprlemladdru  6811  cauappcvgprlem1  6814  caucvgprlemnkj  6821  caucvgprlemnbj  6822  caucvgprlemcl  6831  caucvgprlemladdfu  6832  caucvgprlemladdrl  6833  caucvgprlem1  6834  caucvgprprlemcbv  6842  caucvgprprlemval  6843  caucvgprprlemexb  6862  caucvgprprlem1  6864  addcmpblnr  6881  mulcmpblnrlemg  6882  addsrmo  6885  mulsrmo  6886  addsrpr  6887  mulsrpr  6888  ltsrprg  6889  1idsr  6910  pn0sr  6913  recexgt0sr  6915  mulgt0sr  6919  srpospr  6924  prsradd  6927  caucvgsrlemfv  6932  caucvgsrlemcau  6934  caucvgsrlemgt1  6936  caucvgsrlemoffval  6937  caucvgsrlemoffcau  6939  caucvgsrlemoffres  6941  caucvgsrlembnd  6942  caucvgsr  6943  pitonnlem1p1  6979  pitonnlem2  6980  pitonn  6981  recidpirqlemcalc  6990  ax1rid  7008  axrnegex  7010  axcnre  7012  recriota  7021  nntopi  7025  axcaucvglemval  7028  axcaucvglemcau  7029  axcaucvglemres  7030  mul12  7202  mul4  7205  muladd11  7206  readdcan  7213  muladd11r  7229  add12  7231  cnegex  7251  addcan  7253  negeu  7264  pncan2  7280  addsubass  7283  addsub  7284  2addsub  7287  addsubeq4  7288  subid  7292  subid1  7293  npncan  7294  nppcan  7295  nnpcan  7296  nnncan1  7309  npncan3  7311  pnpcan  7312  pnncan  7314  ppncan  7315  addsub4  7316  negsub  7321  subneg  7322  mvlraddd  7436  mvrraddd  7437  subaddeqd  7438  ine0  7462  mulneg1  7463  ltadd2  7487  apreap  7651  cru  7666  recexap  7707  mulcanapd  7715  div23ap  7743  div13ap  7745  divcanap4  7749  muldivdirap  7757  divsubdirap  7758  divmuldivap  7762  divdivdivap  7763  divcanap5  7764  divmul13ap  7765  divmuleqap  7767  divdiv32ap  7770  divcanap7  7771  dmdcanap  7772  divdivap1  7773  divdivap2  7774  divadddivap  7777  divsubdivap  7778  conjmulap  7779  divneg2ap  7786  mvllmulapd  7883  lt2mul2div  7919  nndivtr  8030  2halves  8210  halfaddsub  8215  avgle1  8221  avgle2  8222  div4p1lem1div2  8234  un0addcl  8271  un0mulcl  8272  peano2z  8337  zneo  8397  nneoor  8398  nneo  8399  zeo  8401  zeo2  8402  deceq1  8430  qreccl  8673  lincmb01cmp  8971  iccf1o  8972  fzosubel3  9153  qavgle  9214  2tnp1ge0ge0  9250  fldiv4p1lem1div2  9254  ceilqm1lt  9261  flqdiv  9270  modqlt  9282  modqdiffl  9284  modqcyc2  9309  modqaddabs  9311  mulqaddmodid  9313  mulp1mod1  9314  modqmuladd  9315  modqmuladdnn0  9317  qnegmod  9318  addmodid  9321  addmodidr  9322  modqadd2mod  9323  modqm1p1mod0  9324  modqmul12d  9327  modqnegd  9328  modqadd12d  9329  modqsub12d  9330  q2submod  9334  modqmulmodr  9339  modqaddmulmod  9340  modqsubdir  9342  modfzo0difsn  9344  modsumfzodifsn  9345  addmodlteq  9347  frecuzrdgsuc  9364  frecfzennn  9366  iseqovex  9382  iseq1p  9402  iseqcaopr2  9404  iseqcaopr  9405  iseqid  9410  iseqhomo  9411  iseqz  9412  expp1  9426  exprecap  9460  expaddzaplem  9462  expmulzap  9465  expdivap  9470  sqval  9477  sqsubswap  9479  subsq  9524  subsq2  9525  binom2  9528  binom2sub  9530  mulbinom2  9532  binom3  9533  zesq  9534  bernneq2  9537  sqoddm1div8  9568  nn0opthlem1d  9587  nn0opthd  9589  nn0opth2d  9590  facp1  9597  facdiv  9605  facndiv  9606  faclbnd  9608  faclbnd2  9609  faclbnd3  9610  bcval  9616  bccmpl  9621  bcm1k  9627  bcp1n  9628  bcp1nk  9629  ibcval5  9630  bcp1m1  9632  bcpasc  9633  bcn2m1  9636  reval  9676  crre  9684  remim  9687  remul2  9700  immul2  9707  imval2  9721  cjdivap  9736  caucvgre  9807  cvg1nlemcau  9810  cvg1nlemres  9811  resqrexlemp1rp  9832  resqrexlemfp1  9835  resqrexlemover  9836  resqrexlemcalc1  9840  resqrexlemcalc3  9842  resqrexlemnm  9844  resqrexlemoverl  9847  resqrexlemglsq  9848  resqrexlemga  9849  resqrexlemsqa  9850  resqrexlemex  9851  resqrex  9852  sqrtdiv  9868  absvalsq  9879  absreimsq  9893  absdivap  9896  cau3lem  9940  clim  10032  clim2  10034  climshftlemg  10053  climshft2  10057  climcn1  10059  climcn2  10060  subcn2  10062  climmulc2  10081  climsubc2  10083  clim2iser  10087  climcau  10096  serif0  10101  moddvds  10116  mulmoddvds  10174  3dvds2dec  10176  zeo3  10178  odd2np1lem  10182  odd2np1  10183  oexpneg  10187  2tp1odd  10195  ltoddhalfle  10204  opoe  10206  opeo  10208  omeo  10209  m1expo  10211  m1exp1  10212  nn0o1gt2  10216  nn0o  10218  divalglemnn  10229  divalglemqt  10230  divalglemeunn  10232  divalglemex  10233  divalglemeuneg  10234  sqr2irrlem  10236  oddpwdclemxy  10243  oddpwdclemndvds  10245
  Copyright terms: Public domain W3C validator