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

Theorem oveq12d 5561
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 5552 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
41, 2, 3syl2anc 403 1 (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1285  (class class class)co 5543
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-rex 2355  df-v 2604  df-un 2978  df-sn 3412  df-pr 3413  df-op 3415  df-uni 3610  df-br 3794  df-iota 4897  df-fv 4940  df-ov 5546
This theorem is referenced by:  oveq123d  5564  ovmpt2dxf  5657  ovmpt2df  5663  caovdig  5706  caovdir2d  5708  caovdirg  5709  caovdilemd  5723  caovlem2d  5724  offval  5750  fnofval  5752  offval2  5757  ofco  5760  caofinvl  5764  offres  5793  nnmsucr  6132  nndir  6134  ecovdi  6283  ecovidi  6284  dfplpq2  6606  dfmpq2  6607  addcmpblnq  6619  mulpipqqs  6625  addassnqg  6634  distrnqg  6639  ltaddnq  6659  halfnqq  6662  enq0tr  6686  addcmpblnq0  6695  addnq0mo  6699  addnnnq0  6701  nqnq0a  6706  distrnq0  6711  addassnq0  6714  distnq0r  6715  nq02m  6717  ltexpri  6865  cauappcvgprlemm  6897  cauappcvgprlemloc  6904  cauappcvgprlemladdru  6908  cauappcvgprlemladdrl  6909  cauappcvgprlem1  6911  cauappcvgprlem2  6912  cauappcvgprlemlim  6913  cauappcvgpr  6914  caucvgprlemnkj  6918  caucvgprlemnbj  6919  caucvgprlemm  6920  caucvgprlemloc  6927  caucvgprlemcl  6928  caucvgprlemladdfu  6929  caucvgprlemladdrl  6930  caucvgprlem2  6932  caucvgpr  6934  caucvgprprlemelu  6938  caucvgprprlemcbv  6939  caucvgprprlemval  6940  caucvgprprlemmu  6947  caucvgprprlemopu  6951  caucvgprprlemloc  6955  caucvgprprlemclphr  6957  caucvgprprlemexbt  6958  caucvgprprlem2  6962  mulcmpblnrlemg  6979  mulsrmo  6983  mulsrpr  6985  mulcomsrg  6996  distrsrg  6998  recexgt0sr  7012  mulgt0sr  7016  mulextsr1lem  7018  caucvgsrlemgt1  7033  caucvgsr  7040  addcnsr  7064  mulcnsr  7065  recidpirqlemcalc  7087  axaddcl  7094  axmulcl  7096  axmulcom  7099  axmulass  7101  axdistr  7102  axcaucvglemcau  7126  axcaucvglemres  7127  adddir  7172  muladd11  7308  1p1times  7309  muladd11r  7331  pnpcan2  7415  muladd  7555  subdir  7557  mulsub  7572  mulreim  7771  apadd1  7775  mulext1  7779  recextlem1  7808  muleqadd  7825  divdirap  7852  divadddivap  7882  conjmulap  7884  divcanap5rd  7971  xp1d2m1eqxm1d2  8350  div4p1lem1div2  8351  cnref1o  8814  icoshftf1o  9089  lincmb01cmp  9101  iccf1o  9102  fz01en  9148  fzrev3  9180  fzrevral2  9199  fzrevral3  9200  fzshftral  9201  fzoaddel2  9279  fzosubel  9280  fzosubel2  9281  fzocatel  9285  modqsubdir  9475  addmodlteq  9480  frecuzrdgsuc  9496  frecfzen2  9509  iseqovex  9529  iseqcaopr3  9556  iseqid3s  9562  iseqdistr  9567  serile  9571  mulexp  9612  mulexpzap  9613  expaddzap  9617  expubnd  9630  subsq  9678  binom2  9682  binom21  9683  binom2sub  9684  binom3  9687  sqoddm1div8  9722  nn0opthlem1d  9744  nn0opthd  9746  facp1  9754  facubnd  9769  bcval  9773  bcn1  9782  bcm1k  9784  bcp1n  9785  bcp1nk  9786  ibcval5  9787  bcn2  9788  bcpasc  9790  sizeun  9829  crre  9882  replim  9884  remullem  9896  remul2  9898  immul2  9905  cjcj  9908  cjadd  9909  ipcnval  9911  cjmulval  9913  cjneg  9915  imval2  9919  cjreim  9928  cvg1nlemcau  10008  cvg1nlemres  10009  resqrexlemp1rp  10030  resqrexlemfp1  10033  resqrexlemcalc1  10038  resqrexlemcalc2  10039  resqrex  10050  sqabsadd  10079  sqabssub  10080  absreimsq  10091  recan  10133  amgm2  10142  maxabslemab  10230  maxabslemval  10232  max0addsup  10243  subcn2  10288  climle  10310  climcvg1nlem  10324  serif0  10327  dvds2ln  10373  odd2np1lem  10416  gcdaddm  10519  bezoutlemnewy  10529  dfgcd3  10543  dvdsgcd  10545  mulgcd  10549  mulgcdr  10551  gcddiv  10552  sqgcd  10562  lcmgcdlem  10603  lcmgcd  10604  qredeu  10623  divgcdcoprm0  10627  cncongr1  10629  oddpwdclemdc  10695  sqrt2irraplemnn  10701
  Copyright terms: Public domain W3C validator