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

Theorem oveq12d 5792
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  |-  ( ph  ->  A  =  B )
oveq12d.2  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
oveq12d  |-  ( ph  ->  ( A F C )  =  ( B F D ) )

Proof of Theorem oveq12d
StepHypRef Expression
1 oveq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 oveq12d.2 . 2  |-  ( ph  ->  C  =  D )
3 oveq12 5783 . 2  |-  ( ( A  =  B  /\  C  =  D )  ->  ( A F C )  =  ( B F D ) )
41, 2, 3syl2anc 408 1  |-  ( ph  ->  ( A F C )  =  ( B F D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1331  (class class class)co 5774
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 3737  df-br 3930  df-iota 5088  df-fv 5131  df-ov 5777
This theorem is referenced by:  oveq123d  5795  ovmpodxf  5896  ovmpodf  5902  caovdig  5945  caovdir2d  5947  caovdirg  5948  caovdilemd  5962  caovlem2d  5963  offval  5989  ofvalg  5991  offval2  5997  ofco  6000  caofinvl  6004  offres  6033  nnmsucr  6384  nndir  6386  ecovdi  6540  ecovidi  6541  dfplpq2  7174  dfmpq2  7175  addcmpblnq  7187  mulpipqqs  7193  addassnqg  7202  distrnqg  7207  ltaddnq  7227  halfnqq  7230  enq0tr  7254  addcmpblnq0  7263  addnq0mo  7267  addnnnq0  7269  nqnq0a  7274  distrnq0  7279  addassnq0  7282  distnq0r  7283  nq02m  7285  ltexpri  7433  cauappcvgprlemm  7465  cauappcvgprlemloc  7472  cauappcvgprlemladdru  7476  cauappcvgprlemladdrl  7477  cauappcvgprlem1  7479  cauappcvgprlem2  7480  cauappcvgprlemlim  7481  cauappcvgpr  7482  caucvgprlemnkj  7486  caucvgprlemnbj  7487  caucvgprlemm  7488  caucvgprlemloc  7495  caucvgprlemcl  7496  caucvgprlemladdfu  7497  caucvgprlemladdrl  7498  caucvgprlem2  7500  caucvgpr  7502  caucvgprprlemelu  7506  caucvgprprlemcbv  7507  caucvgprprlemval  7508  caucvgprprlemmu  7515  caucvgprprlemopu  7519  caucvgprprlemloc  7523  caucvgprprlemclphr  7525  caucvgprprlemexbt  7526  caucvgprprlem2  7530  mulcmpblnrlemg  7560  mulsrmo  7564  mulsrpr  7566  mulcomsrg  7577  distrsrg  7579  recexgt0sr  7593  mulgt0sr  7598  mulextsr1lem  7600  caucvgsrlemgt1  7615  caucvgsr  7622  addcnsr  7654  mulcnsr  7655  recidpirqlemcalc  7677  axaddcl  7684  axmulcl  7686  axmulcom  7691  axmulass  7693  axdistr  7694  axcaucvglemcau  7718  axcaucvglemres  7719  adddir  7769  muladd11  7907  1p1times  7908  muladd11r  7930  pnpcan2  8014  muladd  8158  subdir  8160  mulsub  8175  mulreim  8378  apadd1  8382  mulext1  8386  recextlem1  8424  muleqadd  8441  divdirap  8469  divadddivap  8499  conjmulap  8501  divcanap5rd  8590  subrecap  8610  xp1d2m1eqxm1d2  8984  div4p1lem1div2  8985  cnref1o  9452  xnegid  9654  xposdif  9677  xleaddadd  9682  icoshftf1o  9786  lincmb01cmp  9798  iccf1o  9799  fz01en  9845  fzrev3  9879  fzrevral2  9898  fzrevral3  9899  fzshftral  9900  fzoaddel2  9982  fzosubel  9983  fzosubel2  9984  fzocatel  9988  modqsubdir  10178  addmodlteq  10183  frecuzrdgsuc  10199  frecfzen2  10212  iseqovex  10241  seqvalcd  10244  seq3caopr3  10266  seq3f1olemqsumkj  10283  seq3f1olemqsumk  10284  seq3f1olemqsum  10285  seq3id3  10292  seqfeq3  10297  seq3distr  10298  ser3le  10303  mulexp  10344  mulexpzap  10345  expaddzap  10349  expubnd  10362  subsq  10411  binom2  10415  binom21  10416  binom2sub  10417  binom2sub1  10418  binom3  10421  sqoddm1div8  10456  nn0opthlem1d  10478  nn0opthd  10480  facp1  10488  facubnd  10503  bcval  10507  bcn1  10516  bcm1k  10518  bcp1n  10519  bcp1nk  10520  bcval5  10521  bcn2  10522  bcpasc  10524  hashun  10563  hashfz  10579  crre  10641  replim  10643  remullem  10655  remul2  10657  immul2  10664  cjcj  10667  cjadd  10668  ipcnval  10670  cjmulval  10672  cjneg  10674  imval2  10678  cjreim  10687  cvg1nlemcau  10768  cvg1nlemres  10769  resqrexlemp1rp  10790  resqrexlemfp1  10793  resqrexlemcalc1  10798  resqrexlemcalc2  10799  resqrex  10810  sqabsadd  10839  sqabssub  10840  absreimsq  10851  recan  10893  amgm2  10902  maxabslemab  10990  maxabslemval  10992  max0addsup  11003  minabs  11019  bdtrilem  11022  bdtri  11023  xrmaxadd  11042  xrminadd  11056  xrbdtri  11057  subcn2  11092  reccn2ap  11094  climle  11115  climcvg1nlem  11130  serf0  11133  fsumadd  11187  fsumsplit  11188  sumpr  11194  sumtp  11195  isumadd  11212  sumsplitdc  11213  fsum2dlemstep  11215  fsumshftm  11226  fisumrev2  11227  fsumconst  11235  modfsummodlemstep  11238  telfsumo  11247  fsumparts  11251  binomlem  11264  binom  11265  binom1dif  11268  bcxmaslem1  11269  isumsplit  11272  isumnn0nn  11274  arisum  11279  arisum2  11280  trireciplem  11281  trirecip  11282  geosergap  11287  geo2sum  11295  geo2sum2  11296  cvgratnnlemsumlt  11309  mertenslemi1  11316  mertensabs  11318  eftabs  11374  eftvalcn  11375  efcllemp  11376  ege2le3  11389  efcj  11391  efaddlem  11392  efsep  11409  ef4p  11412  efgt1p2  11413  efgt1p  11414  sinval  11420  cosval  11421  tanvalap  11426  tanval2ap  11431  tanval3ap  11432  efi4p  11435  sinneg  11444  cosneg  11445  tannegap  11446  efival  11450  efmival  11451  sinadd  11454  cosadd  11455  tanaddaplem  11456  tanaddap  11457  sinsub  11458  cossub  11459  addsin  11460  subsin  11461  sinmul  11462  cosmul  11463  addcos  11464  subcos  11465  sincossq  11466  cos2t  11468  sin01bnd  11475  cos01bnd  11476  efieq1re  11489  demoivreALT  11491  dvds2ln  11537  odd2np1lem  11580  gcdaddm  11683  bezoutlemnewy  11695  dfgcd3  11709  dvdsgcd  11711  mulgcd  11715  mulgcdr  11717  gcddiv  11718  sqgcd  11728  lcmgcdlem  11769  lcmgcd  11770  qredeu  11789  divgcdcoprm0  11793  cncongr1  11795  oddpwdclemdc  11862  sqrt2irraplemnn  11868  qnumdenbi  11881  zgcdsq  11890  hashdvds  11908  phiprmpw  11909  phimullem  11912  ennnfonelemp1  11930  ressid2  12032  ressval2  12033  topnvalg  12146  topnpropgd  12148  cnfval  12377  cnpfval  12378  ispsmet  12506  psmet0  12510  psmettri2  12511  psmetres2  12516  ismet  12527  isxmet  12528  xmettri2  12544  xmetres2  12562  xblss2  12588  xmstri2  12653  mstri2  12654  xmstri  12655  mstri  12656  xmstri3  12657  mstri3  12658  msrtri  12659  comet  12682  bdxmet  12684  txmetcnp  12701  metcnpd  12703  cnmet  12713  ioo2bl  12726  fsumcncntop  12739  elcncf  12743  mulc1cncf  12759  cncfco  12761  cncfcncntop  12763  cncfmptc  12765  cncfmptid  12766  addccncf  12769  cdivcncfap  12770  negcncf  12771  mulcncflem  12773  limccnp2cntop  12829  reldvg  12831  dvfvalap  12833  eldvap  12834  dvconst  12844  dvaddxxbr  12848  dvmulxxbr  12849  dvcoapbr  12854  dvcjbr  12855  dvexp  12858  dvrecap  12860  dveflem  12870  dvef  12871  sinperlem  12911  sinmpi  12918  cosmpi  12919  sinppi  12920  cosppi  12921  efimpi  12922  sinhalfpip  12923  sinhalfpim  12924  coshalfpip  12925  coshalfpim  12926  ptolemy  12927  tangtx  12941  logdivlti  12979  cvgcmp2nlemabs  13288  trilpolemclim  13290  trilpolemcl  13291  trilpolemisumle  13292  trilpolemeq1  13294  trilpolemlt1  13295  trilpo  13297
  Copyright terms: Public domain W3C validator