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

Theorem oveq12d 5795
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 5786 . 2 ((𝐴 = 𝐵𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
41, 2, 3syl2anc 408 1 (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1331  (class class class)co 5777
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-rex 2422  df-v 2688  df-un 3075  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3740  df-br 3933  df-iota 5091  df-fv 5134  df-ov 5780
This theorem is referenced by:  oveq123d  5798  ovmpodxf  5899  ovmpodf  5905  caovdig  5948  caovdir2d  5950  caovdirg  5951  caovdilemd  5965  caovlem2d  5966  offval  5992  ofvalg  5994  offval2  6000  ofco  6003  caofinvl  6007  offres  6036  nnmsucr  6387  nndir  6389  ecovdi  6543  ecovidi  6544  dfplpq2  7181  dfmpq2  7182  addcmpblnq  7194  mulpipqqs  7200  addassnqg  7209  distrnqg  7214  ltaddnq  7234  halfnqq  7237  enq0tr  7261  addcmpblnq0  7270  addnq0mo  7274  addnnnq0  7276  nqnq0a  7281  distrnq0  7286  addassnq0  7289  distnq0r  7290  nq02m  7292  ltexpri  7440  cauappcvgprlemm  7472  cauappcvgprlemloc  7479  cauappcvgprlemladdru  7483  cauappcvgprlemladdrl  7484  cauappcvgprlem1  7486  cauappcvgprlem2  7487  cauappcvgprlemlim  7488  cauappcvgpr  7489  caucvgprlemnkj  7493  caucvgprlemnbj  7494  caucvgprlemm  7495  caucvgprlemloc  7502  caucvgprlemcl  7503  caucvgprlemladdfu  7504  caucvgprlemladdrl  7505  caucvgprlem2  7507  caucvgpr  7509  caucvgprprlemelu  7513  caucvgprprlemcbv  7514  caucvgprprlemval  7515  caucvgprprlemmu  7522  caucvgprprlemopu  7526  caucvgprprlemloc  7530  caucvgprprlemclphr  7532  caucvgprprlemexbt  7533  caucvgprprlem2  7537  mulcmpblnrlemg  7567  mulsrmo  7571  mulsrpr  7573  mulcomsrg  7584  distrsrg  7586  recexgt0sr  7600  mulgt0sr  7605  mulextsr1lem  7607  caucvgsrlemgt1  7622  caucvgsr  7629  addcnsr  7661  mulcnsr  7662  recidpirqlemcalc  7684  axaddcl  7691  axmulcl  7693  axmulcom  7698  axmulass  7700  axdistr  7701  axcaucvglemcau  7725  axcaucvglemres  7726  adddir  7776  muladd11  7914  1p1times  7915  muladd11r  7937  pnpcan2  8021  muladd  8165  subdir  8167  mulsub  8182  mulreim  8385  apadd1  8389  mulext1  8393  recextlem1  8431  muleqadd  8448  divdirap  8476  divadddivap  8506  conjmulap  8508  divcanap5rd  8597  subrecap  8617  xp1d2m1eqxm1d2  8991  div4p1lem1div2  8992  cnref1o  9462  xnegid  9665  xposdif  9688  xleaddadd  9693  icoshftf1o  9797  lincmb01cmp  9809  iccf1o  9810  fz01en  9857  fzrev3  9891  fzrevral2  9910  fzrevral3  9911  fzshftral  9912  fzoaddel2  9994  fzosubel  9995  fzosubel2  9996  fzocatel  10000  modqsubdir  10190  addmodlteq  10195  frecuzrdgsuc  10211  frecfzen2  10224  iseqovex  10253  seqvalcd  10256  seq3caopr3  10278  seq3f1olemqsumkj  10295  seq3f1olemqsumk  10296  seq3f1olemqsum  10297  seq3id3  10304  seqfeq3  10309  seq3distr  10310  ser3le  10315  mulexp  10356  mulexpzap  10357  expaddzap  10361  expubnd  10374  subsq  10423  binom2  10427  binom21  10428  binom2sub  10429  binom2sub1  10430  binom3  10433  sqoddm1div8  10468  nn0opthlem1d  10490  nn0opthd  10492  facp1  10500  facubnd  10515  bcval  10519  bcn1  10528  bcm1k  10530  bcp1n  10531  bcp1nk  10532  bcval5  10533  bcn2  10534  bcpasc  10536  hashun  10575  hashfz  10591  crre  10653  replim  10655  remullem  10667  remul2  10669  immul2  10676  cjcj  10679  cjadd  10680  ipcnval  10682  cjmulval  10684  cjneg  10686  imval2  10690  cjreim  10699  cvg1nlemcau  10780  cvg1nlemres  10781  resqrexlemp1rp  10802  resqrexlemfp1  10805  resqrexlemcalc1  10810  resqrexlemcalc2  10811  resqrex  10822  sqabsadd  10851  sqabssub  10852  absreimsq  10863  recan  10905  amgm2  10914  maxabslemab  11002  maxabslemval  11004  max0addsup  11015  minabs  11031  bdtrilem  11034  bdtri  11035  xrmaxadd  11054  xrminadd  11068  xrbdtri  11069  subcn2  11104  reccn2ap  11106  climle  11127  climcvg1nlem  11142  serf0  11145  fsumadd  11199  fsumsplit  11200  sumpr  11206  sumtp  11207  isumadd  11224  sumsplitdc  11225  fsum2dlemstep  11227  fsumshftm  11238  fisumrev2  11239  fsumconst  11247  modfsummodlemstep  11250  telfsumo  11259  fsumparts  11263  binomlem  11276  binom  11277  binom1dif  11280  bcxmaslem1  11281  isumsplit  11284  isumnn0nn  11286  arisum  11291  arisum2  11292  trireciplem  11293  trirecip  11294  geosergap  11299  geo2sum  11307  geo2sum2  11308  cvgratnnlemsumlt  11321  mertenslemi1  11328  mertensabs  11330  eftabs  11386  eftvalcn  11387  efcllemp  11388  ege2le3  11401  efcj  11403  efaddlem  11404  efsep  11421  ef4p  11424  efgt1p2  11425  efgt1p  11426  sinval  11432  cosval  11433  tanvalap  11438  tanval2ap  11443  tanval3ap  11444  efi4p  11447  sinneg  11456  cosneg  11457  tannegap  11458  efival  11462  efmival  11463  sinadd  11466  cosadd  11467  tanaddaplem  11468  tanaddap  11469  sinsub  11470  cossub  11471  addsin  11472  subsin  11473  sinmul  11474  cosmul  11475  addcos  11476  subcos  11477  sincossq  11478  cos2t  11480  sin01bnd  11487  cos01bnd  11488  efieq1re  11501  demoivreALT  11503  dvds2ln  11549  odd2np1lem  11592  gcdaddm  11695  bezoutlemnewy  11707  dfgcd3  11721  dvdsgcd  11723  mulgcd  11727  mulgcdr  11729  gcddiv  11730  sqgcd  11740  lcmgcdlem  11781  lcmgcd  11782  qredeu  11801  divgcdcoprm0  11805  cncongr1  11807  oddpwdclemdc  11874  sqrt2irraplemnn  11880  qnumdenbi  11893  zgcdsq  11902  hashdvds  11920  phiprmpw  11921  phimullem  11924  ennnfonelemp1  11942  ressid2  12044  ressval2  12045  topnvalg  12158  topnpropgd  12160  cnfval  12389  cnpfval  12390  ispsmet  12518  psmet0  12522  psmettri2  12523  psmetres2  12528  ismet  12539  isxmet  12540  xmettri2  12556  xmetres2  12574  xblss2  12600  xmstri2  12665  mstri2  12666  xmstri  12667  mstri  12668  xmstri3  12669  mstri3  12670  msrtri  12671  comet  12694  bdxmet  12696  txmetcnp  12713  metcnpd  12715  cnmet  12725  ioo2bl  12738  fsumcncntop  12751  elcncf  12755  mulc1cncf  12771  cncfco  12773  cncfcncntop  12775  cncfmptc  12777  cncfmptid  12778  addccncf  12781  cdivcncfap  12782  negcncf  12783  mulcncflem  12785  limccnp2cntop  12841  reldvg  12843  dvfvalap  12845  eldvap  12846  dvconst  12856  dvaddxxbr  12860  dvmulxxbr  12861  dvcoapbr  12866  dvcjbr  12867  dvexp  12870  dvrecap  12872  dveflem  12882  dvef  12883  sinperlem  12923  sinmpi  12930  cosmpi  12931  sinppi  12932  cosppi  12933  efimpi  12934  sinhalfpip  12935  sinhalfpim  12936  coshalfpip  12937  coshalfpim  12938  ptolemy  12939  tangtx  12953  logdivlti  12996  rpcxpadd  13020  rpmulcxp  13024  rplogbchbase  13060  rprelogbmul  13065  cvgcmp2nlemabs  13375  trilpolemclim  13377  trilpolemcl  13378  trilpolemisumle  13379  trilpolemeq1  13381  trilpolemlt1  13382  trilpo  13384  redcwlpo  13395  neapmkv  13398
  Copyright terms: Public domain W3C validator