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

Theorem oveq1d 5505
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 5497 . 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 1243  (class class class)co 5490
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-rex 2309  df-v 2556  df-un 2919  df-sn 3378  df-pr 3379  df-op 3381  df-uni 3578  df-br 3762  df-iota 4845  df-fv 4888  df-ov 5493
This theorem is referenced by:  csbov2g  5524  caovassg  5637  caovdig  5653  caovdirg  5656  caov12d  5660  caov31d  5661  caov411d  5664  grprinvlem  5673  grprinvd  5674  grpridd  5675  caofinvl  5711  omsuc  6029  nnmsucr  6045  nnm1  6075  nnm2  6076  ecovass  6193  ecoviass  6194  ecovdi  6195  ecovidi  6196  addasspig  6400  mulasspig  6402  mulpipq2  6441  distrnqg  6457  ltsonq  6468  ltanqg  6470  ltmnqg  6471  ltexnqq  6478  archnqq  6487  prarloclemarch2  6489  enq0sym  6502  addnq0mo  6517  mulnq0mo  6518  addnnnq0  6519  nqpnq0nq  6523  nq0m0r  6526  nq0a0  6527  nnanq0  6528  distrnq0  6529  addassnq0  6532  addpinq1  6534  prarloclemlo  6564  prarloclem3  6567  prarloclem5  6570  prarloclemcalc  6572  addnqprllem  6597  addnqprulem  6598  appdivnq  6633  recexprlem1ssl  6703  recexprlem1ssu  6704  ltmprr  6712  cauappcvgprlemladdru  6726  cauappcvgprlem1  6729  caucvgprlemnkj  6736  caucvgprlemnbj  6737  caucvgprlemcl  6746  caucvgprlemladdfu  6747  caucvgprlemladdrl  6748  caucvgprlem1  6749  caucvgprprlemcbv  6757  caucvgprprlemval  6758  caucvgprprlemexb  6777  caucvgprprlem1  6779  addcmpblnr  6796  mulcmpblnrlemg  6797  addsrmo  6800  mulsrmo  6801  addsrpr  6802  mulsrpr  6803  ltsrprg  6804  1idsr  6825  pn0sr  6828  recexgt0sr  6830  mulgt0sr  6834  srpospr  6839  prsradd  6842  caucvgsrlemfv  6847  caucvgsrlemcau  6849  caucvgsrlemgt1  6851  caucvgsrlemoffval  6852  caucvgsrlemoffcau  6854  caucvgsrlemoffres  6856  caucvgsrlembnd  6857  caucvgsr  6858  pitonnlem1p1  6894  pitonnlem2  6895  pitonn  6896  recidpirqlemcalc  6905  ax1rid  6923  axrnegex  6925  axcnre  6927  recriota  6936  nntopi  6940  axcaucvglemval  6943  axcaucvglemcau  6944  axcaucvglemres  6945  mul12  7113  mul4  7116  muladd11  7117  readdcan  7124  add12  7140  cnegex  7160  addcan  7162  negeu  7173  pncan2  7189  addsubass  7192  addsub  7193  2addsub  7196  addsubeq4  7197  subid  7200  subid1  7201  npncan  7202  nppcan  7203  nnpcan  7204  nnncan1  7217  npncan3  7219  pnpcan  7220  pnncan  7222  ppncan  7223  addsub4  7224  negsub  7229  subneg  7230  ine0  7361  mulneg1  7362  ltadd2  7386  apreap  7545  cru  7560  recexap  7601  mulcanapd  7609  div23ap  7637  div13ap  7639  divcanap4  7643  divsubdirap  7651  divmuldivap  7655  divdivdivap  7656  divcanap5  7657  divmul13ap  7658  divmuleqap  7660  divdiv32ap  7663  divcanap7  7664  dmdcanap  7665  divdivap1  7666  divdivap2  7667  divadddivap  7670  divsubdivap  7671  conjmulap  7672  divneg2ap  7679  mvllmulapd  7776  lt2mul2div  7812  nndivtr  7922  2halves  8118  halfaddsub  8123  avgle1  8129  avgle2  8130  un0addcl  8178  un0mulcl  8179  peano2z  8244  zneo  8302  nneoor  8303  nneo  8304  zeo  8306  zeo2  8307  deceq1  8333  qreccl  8538  lincmb01cmp  8829  iccf1o  8830  fzosubel3  9010  frecuzrdgsuc  9070  frecfzennn  9072  iseqovex  9088  iseq1p  9108  iseqcaopr2  9110  iseqcaopr  9111  iseqid  9116  iseqhomo  9117  expp1  9131  exprecap  9165  expaddzaplem  9167  expmulzap  9170  expdivap  9174  sqval  9181  sqsubswap  9183  subsq  9227  subsq2  9228  binom2  9231  binom2sub  9233  binom3  9235  zesq  9236  bernneq2  9239  reval  9318  crre  9326  remim  9329  remul2  9342  immul2  9349  imval2  9363  cjdivap  9378  caucvgre  9449  cvg1nlemcau  9452  cvg1nlemres  9453  resqrexlemp1rp  9473  resqrexlemfp1  9476  resqrexlemover  9477  resqrexlemcalc1  9481  resqrexlemcalc3  9483  resqrexlemnm  9485  resqrexlemoverl  9488  resqrexlemglsq  9489  resqrexlemga  9490  resqrexlemsqa  9491  resqrexlemex  9492  resqrex  9493  sqrtdiv  9509  absvalsq  9520  absreimsq  9534  absdivap  9537  cau3lem  9579  clim  9670  clim2  9672  climshftlemg  9691  climshft2  9695  climcn1  9697  climcn2  9698  subcn2  9700  climmulc2  9719  climsubc2  9721  clim2iser  9725  climcau  9734  serif0  9739  sqr2irrlem  9745
  Copyright terms: Public domain W3C validator