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

Theorem oveq12d 5517
Description: Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
Hypotheses
Ref Expression
oveq1d.1 (𝜑𝐴 = 𝐵)
oveq12d.2 (𝜑𝐶 = 𝐷)
Assertion
Ref Expression
oveq12d (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))

Proof of Theorem oveq12d
StepHypRef Expression
1 oveq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 oveq12d.2 . 2 (𝜑𝐶 = 𝐷)
3 oveq12 5508 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
41, 2, 3syl2anc 391 1 (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1243  (class class class)co 5499
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 4854  df-fv 4897  df-ov 5502
This theorem is referenced by:  oveq123d  5520  ovmpt2dxf  5613  ovmpt2df  5619  caovdig  5662  caovdir2d  5664  caovdirg  5665  caovdilemd  5679  caovlem2d  5680  offval  5706  fnofval  5708  offval2  5713  ofco  5716  caofinvl  5720  offres  5749  nnmsucr  6054  nndir  6056  ecovdi  6204  ecovidi  6205  dfplpq2  6433  dfmpq2  6434  addcmpblnq  6446  mulpipqqs  6452  addassnqg  6461  distrnqg  6466  ltaddnq  6486  halfnqq  6489  enq0tr  6513  addcmpblnq0  6522  addnq0mo  6526  addnnnq0  6528  nqnq0a  6533  distrnq0  6538  addassnq0  6541  distnq0r  6542  nq02m  6544  ltexpri  6692  cauappcvgprlemm  6724  cauappcvgprlemloc  6731  cauappcvgprlemladdru  6735  cauappcvgprlemladdrl  6736  cauappcvgprlem1  6738  cauappcvgprlem2  6739  cauappcvgprlemlim  6740  cauappcvgpr  6741  caucvgprlemnkj  6745  caucvgprlemnbj  6746  caucvgprlemm  6747  caucvgprlemloc  6754  caucvgprlemcl  6755  caucvgprlemladdfu  6756  caucvgprlemladdrl  6757  caucvgprlem2  6759  caucvgpr  6761  caucvgprprlemelu  6765  caucvgprprlemcbv  6766  caucvgprprlemval  6767  caucvgprprlemmu  6774  caucvgprprlemopu  6778  caucvgprprlemloc  6782  caucvgprprlemclphr  6784  caucvgprprlemexbt  6785  caucvgprprlem2  6789  mulcmpblnrlemg  6806  mulsrmo  6810  mulsrpr  6812  mulcomsrg  6823  distrsrg  6825  recexgt0sr  6839  mulgt0sr  6843  mulextsr1lem  6845  caucvgsrlemgt1  6860  caucvgsr  6867  addcnsr  6891  mulcnsr  6892  recidpirqlemcalc  6914  axaddcl  6921  axmulcl  6923  axmulcom  6926  axmulass  6928  axdistr  6929  axcaucvglemcau  6953  axcaucvglemres  6954  adddir  6999  muladd11  7126  1p1times  7127  pnpcan2  7230  muladd  7360  subdir  7362  mulsub  7377  mulreim  7571  apadd1  7575  mulext1  7579  recextlem1  7608  muleqadd  7625  divdirap  7650  divadddivap  7679  conjmulap  7681  divcanap5rd  7768  cnref1o  8553  icoshftf1o  8826  lincmb01cmp  8838  iccf1o  8839  fz01en  8884  fzrev3  8916  fzrevral2  8935  fzrevral3  8936  fzshftral  8937  fzoaddel2  9016  fzosubel  9017  fzosubel2  9018  fzocatel  9022  frecuzrdgsuc  9079  frecfzen2  9082  iseqovex  9097  iseqcaopr3  9118  iseqid3s  9124  iseqdistr  9127  serile  9131  mulexp  9172  mulexpzap  9173  expaddzap  9177  expubnd  9189  subsq  9236  binom2  9240  binom21  9241  binom2sub  9242  binom3  9244  crre  9335  replim  9337  remullem  9349  remul2  9351  immul2  9358  cjcj  9361  cjadd  9362  ipcnval  9364  cjmulval  9366  cjneg  9368  imval2  9372  cjreim  9381  cvg1nlemcau  9461  cvg1nlemres  9462  resqrexlemp1rp  9482  resqrexlemfp1  9485  resqrexlemcalc1  9490  resqrexlemcalc2  9491  resqrex  9502  sqabsadd  9531  sqabssub  9532  absreimsq  9543  recan  9583  amgm2  9592  subcn2  9709  climle  9731  climcvg1nlem  9745  serif0  9748
  Copyright terms: Public domain W3C validator