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

Theorem oveq12d 5633
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 5624 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
41, 2, 3syl2anc 403 1 (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1287  (class class class)co 5615
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 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-3an 924  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-rex 2361  df-v 2617  df-un 2992  df-sn 3437  df-pr 3438  df-op 3440  df-uni 3639  df-br 3823  df-iota 4948  df-fv 4991  df-ov 5618
This theorem is referenced by:  oveq123d  5636  ovmpt2dxf  5729  ovmpt2df  5735  caovdig  5778  caovdir2d  5780  caovdirg  5781  caovdilemd  5795  caovlem2d  5796  offval  5822  fnofval  5824  offval2  5829  ofco  5832  caofinvl  5836  offres  5865  nnmsucr  6205  nndir  6207  ecovdi  6357  ecovidi  6358  dfplpq2  6860  dfmpq2  6861  addcmpblnq  6873  mulpipqqs  6879  addassnqg  6888  distrnqg  6893  ltaddnq  6913  halfnqq  6916  enq0tr  6940  addcmpblnq0  6949  addnq0mo  6953  addnnnq0  6955  nqnq0a  6960  distrnq0  6965  addassnq0  6968  distnq0r  6969  nq02m  6971  ltexpri  7119  cauappcvgprlemm  7151  cauappcvgprlemloc  7158  cauappcvgprlemladdru  7162  cauappcvgprlemladdrl  7163  cauappcvgprlem1  7165  cauappcvgprlem2  7166  cauappcvgprlemlim  7167  cauappcvgpr  7168  caucvgprlemnkj  7172  caucvgprlemnbj  7173  caucvgprlemm  7174  caucvgprlemloc  7181  caucvgprlemcl  7182  caucvgprlemladdfu  7183  caucvgprlemladdrl  7184  caucvgprlem2  7186  caucvgpr  7188  caucvgprprlemelu  7192  caucvgprprlemcbv  7193  caucvgprprlemval  7194  caucvgprprlemmu  7201  caucvgprprlemopu  7205  caucvgprprlemloc  7209  caucvgprprlemclphr  7211  caucvgprprlemexbt  7212  caucvgprprlem2  7216  mulcmpblnrlemg  7233  mulsrmo  7237  mulsrpr  7239  mulcomsrg  7250  distrsrg  7252  recexgt0sr  7266  mulgt0sr  7270  mulextsr1lem  7272  caucvgsrlemgt1  7287  caucvgsr  7294  addcnsr  7318  mulcnsr  7319  recidpirqlemcalc  7341  axaddcl  7348  axmulcl  7350  axmulcom  7353  axmulass  7355  axdistr  7356  axcaucvglemcau  7380  axcaucvglemres  7381  adddir  7426  muladd11  7562  1p1times  7563  muladd11r  7585  pnpcan2  7669  muladd  7809  subdir  7811  mulsub  7826  mulreim  8025  apadd1  8029  mulext1  8033  recextlem1  8062  muleqadd  8079  divdirap  8106  divadddivap  8136  conjmulap  8138  divcanap5rd  8225  xp1d2m1eqxm1d2  8604  div4p1lem1div2  8605  cnref1o  9068  icoshftf1o  9343  lincmb01cmp  9355  iccf1o  9356  fz01en  9402  fzrev3  9434  fzrevral2  9453  fzrevral3  9454  fzshftral  9455  fzoaddel2  9535  fzosubel  9536  fzosubel2  9537  fzocatel  9541  modqsubdir  9731  addmodlteq  9736  frecuzrdgsuc  9752  frecfzen2  9765  iseqovex  9790  iseqcaopr3  9818  iseqf1olemqsumkj  9835  iseqf1olemqsumk  9836  iseqf1olemqsum  9837  iseqid3s  9845  iseqdistr  9850  serile  9855  mulexp  9896  mulexpzap  9897  expaddzap  9901  expubnd  9914  subsq  9962  binom2  9966  binom21  9967  binom2sub  9968  binom3  9971  sqoddm1div8  10006  nn0opthlem1d  10028  nn0opthd  10030  facp1  10038  facubnd  10053  bcval  10057  bcn1  10066  bcm1k  10068  bcp1n  10069  bcp1nk  10070  ibcval5  10071  bcn2  10072  bcpasc  10074  hashun  10113  hashfz  10129  crre  10190  replim  10192  remullem  10204  remul2  10206  immul2  10213  cjcj  10216  cjadd  10217  ipcnval  10219  cjmulval  10221  cjneg  10223  imval2  10227  cjreim  10236  cvg1nlemcau  10316  cvg1nlemres  10317  resqrexlemp1rp  10338  resqrexlemfp1  10341  resqrexlemcalc1  10346  resqrexlemcalc2  10347  resqrex  10358  sqabsadd  10387  sqabssub  10388  absreimsq  10399  recan  10441  amgm2  10450  maxabslemab  10538  maxabslemval  10540  max0addsup  10551  subcn2  10597  climle  10619  climcvg1nlem  10633  serif0  10636  fsumadd  10688  fsumsplit  10689  sumpr  10694  sumtp  10695  dvds2ln  10735  odd2np1lem  10778  gcdaddm  10881  bezoutlemnewy  10891  dfgcd3  10905  dvdsgcd  10907  mulgcd  10911  mulgcdr  10913  gcddiv  10914  sqgcd  10924  lcmgcdlem  10965  lcmgcd  10966  qredeu  10985  divgcdcoprm0  10989  cncongr1  10991  oddpwdclemdc  11057  sqrt2irraplemnn  11063  qnumdenbi  11076  zgcdsq  11085  hashdvds  11103  phiprmpw  11104  phimullem  11107
  Copyright terms: Public domain W3C validator