Theorem oveqan12d 7174

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 7164	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))
4	1, 2, 3	syl2an 598	1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538  (class class class)co 7155

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-un 3865  df-in 3867  df-ss 3877  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-br 5036  df-iota 6298  df-fv 6347  df-ov 7158

This theorem is referenced by:  oveqan12rd  7175  offval  7418  offval3  7692  odi  8220  omopth2  8225  oeoa  8238  ecovdi  8420  ackbij1lem9  9693  distrpi  10363  addpipq  10402  mulpipq  10405  lterpq  10435  reclem3pr  10514  1idsr  10563  mulcnsr  10601  mulid1  10682  1re  10684  mul02  10861  addcom  10869  mulsub  11126  mulsub2  11127  muleqadd  11327  divmuldiv  11383  div2sub  11508  addltmul  11915  xnegdi  12687  xadddilem  12733  fzsubel  12997  fzoval  13093  seqid3  13469  mulexp  13523  sqdiv  13542  hashdom  13795  hashun  13798  ccatfval  13977  splcl  14166  crim  14527  readd  14538  remullem  14540  imadd  14546  cjadd  14553  cjreim  14572  sqrtmul  14672  sqabsadd  14695  sqabssub  14696  absmul  14707  abs2dif  14745  bhmafibid1  14878  binom  15238  binomfallfac  15448  sinadd  15570  cosadd  15571  dvds2ln  15695  sadcaddlem  15861  bezoutlem4  15946  bezout  15947  absmulgcd  15953  gcddiv  15955  bezoutr1  15970  lcmgcd  16008  lcmfass  16047  nn0gcdsq  16152  crth  16175  pythagtriplem1  16213  pcqmul  16250  4sqlem4a  16347  4sqlem4  16348  prdsplusgval  16809  prdsmulrval  16811  prdsdsval  16814  prdsvscaval  16815  idmhm  18036  0mhm  18055  resmhm  18056  prdspjmhm  18064  pwsdiagmhm  18066  gsumws2  18078  frmdup1  18100  eqgval  18401  idghm  18445  resghm  18446  mulgmhm  19021  mulgghm  19022  srglmhm  19358  srgrmhm  19359  ringlghm  19430  ringrghm  19431  gsumdixp  19435  isrhm  19549  issrngd  19705  lmodvsghm  19768  pwssplit2  19905  xrsdsval  20215  expmhm  20240  expghm  20270  mulgghm2  20271  mulgrhm  20272  cygznlem3  20342  asclghm  20650  psrmulfval  20718  evlslem4  20842  mpfrcl  20853  mamuval  21093  mamufv  21094  mvmulval  21248  mndifsplit  21341  mat2pmatmul  21436  decpmatmul  21477  fmval  22648  fmf  22650  flffval  22694  divcn  23574  rescncf  23603  htpyco1  23684  tcphcph  23942  rrxdsfival  24118  ehl2eudisval  24128  volun  24250  dyadval  24297  dvlip  24697  ftc1a  24741  ftc2ditglem  24749  tdeglem3  24762  tdeglem3OLD  24763  q1pval  24858  reefgim  25149  relogoprlem  25286  eflogeq  25297  zetacvg  25704  lgsdir2  26018  lgsdchr  26043  2sq2  26121  2sqnn0  26126  brbtwn2  26803  ax5seglem4  26830  axeuclid  26861  axcontlem2  26863  axcontlem4  26865  axcontlem8  26869  clwwlknccat  27952  ex-fpar  28351  ipasslem11  28727  hhssnv  29151  mayete3i  29615  idunop  29865  idhmop  29869  0lnfn  29872  lnopmi  29887  lnophsi  29888  lnopcoi  29890  hmops  29907  hmopm  29908  nlelshi  29947  cnlnadjlem2  29955  kbass6  30008  strlem3a  30139  hstrlem3a  30147  mndpluscn  31401  xrge0iifhom  31412  rezh  31444  probdsb  31912  resconn  32728  iscvm  32741  satfdmlem  32850  satffunlem1lem1  32884  satffunlem2lem1  32886  fwddifnval  34040  bj-bary1  35032  poimirlem15  35378  mbfposadd  35410  ftc1anclem3  35438  rrnmval  35572  dvhopaddN  38716  nnadddir  39830  cnreeu  39963  pellex  40177  rmxfval  40246  rmyfval  40247  qirropth  40250  rmxycomplete  40259  jm2.15nn0  40345  rmxdioph  40358  expdiophlem2  40364  mendvsca  40536  deg1mhm  40552  mnringmulrvald  41336  addrval  41571  subrval  41572  fmulcl  42617  fmuldfeqlem1  42618  idmgmhm  44803  resmgmhm  44813  rhmval  44938  line  45539  itsclc0xyqsolr  45576