Theorem oveqan12d 7377

Description: Equality deduction for operation value. (Contributed by NM, 10-Aug-1995.)

Hypotheses

Ref	Expression
oveq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)
opreqan12i.2	⊢ (𝜓 → 𝐶 = 𝐷)

Assertion

Ref	Expression
oveqan12d	⊢ ((𝜑 ∧ 𝜓) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))

Proof of Theorem oveqan12d

Step	Hyp	Ref	Expression
1		oveq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		opreqan12i.2	. 2 ⊢ (𝜓 → 𝐶 = 𝐷)
3		oveq12 7367	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
4	1, 2, 3	syl2an 597	1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542  (class class class)co 7358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-rab 3399  df-v 3441  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4285  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-iota 6447  df-fv 6499  df-ov 7361

This theorem is referenced by:  oveqan12rd  7378  offval  7631  offval3  7926  odi  8506  omopth2  8511  oeoa  8525  ecovdi  8764  ackbij1lem9  10139  distrpi  10811  addpipq  10850  mulpipq  10853  lterpq  10883  reclem3pr  10962  1idsr  11011  mulcnsr  11049  mulrid  11132  1re  11134  mul02  11313  addcom  11321  mulsub  11582  mulsub2  11583  muleqadd  11783  divmuldiv  11843  div2sub  11968  addltmul  12379  xnegdi  13165  xadddilem  13211  fzsubel  13478  fzoval  13578  seqid3  13971  mulexp  14026  sqdiv  14046  hashdom  14304  hashun  14307  ccatfval  14498  splcl  14677  crim  15040  readd  15051  remullem  15053  imadd  15059  cjadd  15066  cjreim  15085  sqrtmul  15184  sqabsadd  15207  sqabssub  15208  absmul  15219  abs2dif  15258  bhmafibid1  15393  binom  15755  binomfallfac  15966  sinadd  16091  cosadd  16092  dvds2ln  16218  sadcaddlem  16386  bezoutlem4  16471  bezout  16472  absmulgcd  16478  gcddiv  16480  bezoutr1  16498  lcmgcd  16536  lcmfass  16575  nn0gcdsq  16681  crth  16707  pythagtriplem1  16746  pcqmul  16783  4sqlem4a  16881  4sqlem4  16882  prdsplusgval  17395  prdsmulrval  17397  prdsdsval  17400  prdsvscaval  17401  idmgmhm  18628  resmgmhm  18638  idmhm  18722  0mhm  18746  resmhm  18747  prdspjmhm  18756  pwsdiagmhm  18758  gsumws2  18769  frmdup1  18791  eqgval  19108  idghm  19162  resghm  19163  mulgmhm  19758  mulgghm  19759  srglmhm  20158  srgrmhm  20159  ringlghm  20249  ringrghm  20250  gsumdixp  20256  isrhm  20416  rhmval  20435  issrngd  20790  lmodvsghm  20876  pwssplit2  21014  xrsdsval  21367  expmhm  21393  expghm  21432  mulgghm2  21433  mulgrhm  21434  pzriprnglem4  21441  cygznlem3  21526  asclghm  21840  psrmulfval  21901  evlslem4  22033  mpfrcl  22042  mamuval  22339  mamufv  22340  mvmulval  22489  mndifsplit  22582  mat2pmatmul  22677  decpmatmul  22718  fmval  23889  fmf  23891  flffval  23935  divcnOLD  24815  divcn  24817  rescncf  24848  htpyco1  24935  tcphcph  25195  rrxdsfival  25371  ehl2eudisval  25381  volun  25504  dyadval  25551  dvlip  25956  ftc1a  26002  ftc2ditglem  26010  tdeglem3  26022  q1pval  26118  reefgim  26418  relogoprlem  26558  eflogeq  26569  zetacvg  26983  lgsdir2  27299  lgsdchr  27324  2sq2  27402  2sqnn0  27407  negsdi  28030  brbtwn2  28959  ax5seglem4  28986  axeuclid  29017  axcontlem2  29019  axcontlem4  29021  axcontlem8  29025  clwwlknccat  30119  ex-fpar  30518  ipasslem11  30896  hhssnv  31320  mayete3i  31784  idunop  32034  idhmop  32038  0lnfn  32041  lnopmi  32056  lnophsi  32057  lnopcoi  32059  hmops  32076  hmopm  32077  nlelshi  32116  cnlnadjlem2  32124  kbass6  32177  strlem3a  32308  hstrlem3a  32316  elrgspnlem2  33304  mndpluscn  34062  xrge0iifhom  34073  rezh  34105  probdsb  34558  resconn  35419  iscvm  35432  satfdmlem  35541  satffunlem1lem1  35575  satffunlem2lem1  35577  fwddifnval  36336  bj-bary1  37486  poimirlem15  37805  mbfposadd  37837  ftc1anclem3  37865  rrnmval  37998  dvhopaddN  41409  nnadddir  42562  cnreeu  42782  prjcrvfval  42911  pellex  43114  rmxfval  43183  rmyfval  43184  qirropth  43187  rmxycomplete  43196  jm2.15nn0  43282  rmxdioph  43295  expdiophlem2  43301  mendvsca  43466  deg1mhm  43479  mnringmulrvald  44505  addrval  44743  subrval  44744  fmulcl  45864  fmuldfeqlem1  45865  line  49015  itsclc0xyqsolr  49052