Theorem oveq12d 5625

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

Step	Hyp	Ref	Expression
1		oveq1d.1	. 2 |- ( ph -> A = B )
2		oveq12d.2	. 2 |- ( ph -> C = D )
3		oveq12 5616	. 2 |- ( ( A = B /\ C = D ) -> ( A F C ) = ( B F D ) )
4	1, 2, 3	syl2anc 403	1 |- ( ph -> ( A F C ) = ( B F D ) )

Syntax hints:   -> wi 4   = wceq 1287  (class class class)co 5607

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 3637  df-br 3821  df-iota 4943  df-fv 4986  df-ov 5610

This theorem is referenced by:  oveq123d  5628  ovmpt2dxf  5721  ovmpt2df  5727  caovdig  5770  caovdir2d  5772  caovdirg  5773  caovdilemd  5787  caovlem2d  5788  offval  5814  fnofval  5816  offval2  5821  ofco  5824  caofinvl  5828  offres  5857  nnmsucr  6197  nndir  6199  ecovdi  6349  ecovidi  6350  dfplpq2  6850  dfmpq2  6851  addcmpblnq  6863  mulpipqqs  6869  addassnqg  6878  distrnqg  6883  ltaddnq  6903  halfnqq  6906  enq0tr  6930  addcmpblnq0  6939  addnq0mo  6943  addnnnq0  6945  nqnq0a  6950  distrnq0  6955  addassnq0  6958  distnq0r  6959  nq02m  6961  ltexpri  7109  cauappcvgprlemm  7141  cauappcvgprlemloc  7148  cauappcvgprlemladdru  7152  cauappcvgprlemladdrl  7153  cauappcvgprlem1  7155  cauappcvgprlem2  7156  cauappcvgprlemlim  7157  cauappcvgpr  7158  caucvgprlemnkj  7162  caucvgprlemnbj  7163  caucvgprlemm  7164  caucvgprlemloc  7171  caucvgprlemcl  7172  caucvgprlemladdfu  7173  caucvgprlemladdrl  7174  caucvgprlem2  7176  caucvgpr  7178  caucvgprprlemelu  7182  caucvgprprlemcbv  7183  caucvgprprlemval  7184  caucvgprprlemmu  7191  caucvgprprlemopu  7195  caucvgprprlemloc  7199  caucvgprprlemclphr  7201  caucvgprprlemexbt  7202  caucvgprprlem2  7206  mulcmpblnrlemg  7223  mulsrmo  7227  mulsrpr  7229  mulcomsrg  7240  distrsrg  7242  recexgt0sr  7256  mulgt0sr  7260  mulextsr1lem  7262  caucvgsrlemgt1  7277  caucvgsr  7284  addcnsr  7308  mulcnsr  7309  recidpirqlemcalc  7331  axaddcl  7338  axmulcl  7340  axmulcom  7343  axmulass  7345  axdistr  7346  axcaucvglemcau  7370  axcaucvglemres  7371  adddir  7416  muladd11  7552  1p1times  7553  muladd11r  7575  pnpcan2  7659  muladd  7799  subdir  7801  mulsub  7816  mulreim  8015  apadd1  8019  mulext1  8023  recextlem1  8052  muleqadd  8069  divdirap  8096  divadddivap  8126  conjmulap  8128  divcanap5rd  8215  xp1d2m1eqxm1d2  8594  div4p1lem1div2  8595  cnref1o  9058  icoshftf1o  9333  lincmb01cmp  9345  iccf1o  9346  fz01en  9392  fzrev3  9424  fzrevral2  9443  fzrevral3  9444  fzshftral  9445  fzoaddel2  9525  fzosubel  9526  fzosubel2  9527  fzocatel  9531  modqsubdir  9721  addmodlteq  9726  frecuzrdgsuc  9742  frecfzen2  9755  iseqovex  9780  iseqcaopr3  9807  iseqf1olemqsumkj  9824  iseqf1olemqsumk  9825  iseqf1olemqsum  9826  iseqid3s  9834  iseqdistr  9839  serile  9844  mulexp  9885  mulexpzap  9886  expaddzap  9890  expubnd  9903  subsq  9951  binom2  9955  binom21  9956  binom2sub  9957  binom3  9960  sqoddm1div8  9995  nn0opthlem1d  10017  nn0opthd  10019  facp1  10027  facubnd  10042  bcval  10046  bcn1  10055  bcm1k  10057  bcp1n  10058  bcp1nk  10059  ibcval5  10060  bcn2  10061  bcpasc  10063  hashun  10102  hashfz  10118  crre  10179  replim  10181  remullem  10193  remul2  10195  immul2  10202  cjcj  10205  cjadd  10206  ipcnval  10208  cjmulval  10210  cjneg  10212  imval2  10216  cjreim  10225  cvg1nlemcau  10305  cvg1nlemres  10306  resqrexlemp1rp  10327  resqrexlemfp1  10330  resqrexlemcalc1  10335  resqrexlemcalc2  10336  resqrex  10347  sqabsadd  10376  sqabssub  10377  absreimsq  10388  recan  10430  amgm2  10439  maxabslemab  10527  maxabslemval  10529  max0addsup  10540  subcn2  10585  climle  10607  climcvg1nlem  10621  serif0  10624  dvds2ln  10696  odd2np1lem  10739  gcdaddm  10842  bezoutlemnewy  10852  dfgcd3  10866  dvdsgcd  10868  mulgcd  10872  mulgcdr  10874  gcddiv  10875  sqgcd  10885  lcmgcdlem  10926  lcmgcd  10927  qredeu  10946  divgcdcoprm0  10950  cncongr1  10952  oddpwdclemdc  11018  sqrt2irraplemnn  11024  qnumdenbi  11037  zgcdsq  11046  hashdvds  11064  phiprmpw  11065  phimullem  11068