Theorem oveqan12d 7360

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541  (class class class)co 7341

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3394  df-v 3436  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4282  df-if 4474  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-br 5090  df-iota 6433  df-fv 6485  df-ov 7344

This theorem is referenced by:  oveqan12rd  7361  offval  7614  offval3  7909  odi  8489  omopth2  8494  oeoa  8507  ecovdi  8744  ackbij1lem9  10110  distrpi  10781  addpipq  10820  mulpipq  10823  lterpq  10853  reclem3pr  10932  1idsr  10981  mulcnsr  11019  mulrid  11102  1re  11104  mul02  11283  addcom  11291  mulsub  11552  mulsub2  11553  muleqadd  11753  divmuldiv  11813  div2sub  11938  addltmul  12349  xnegdi  13139  xadddilem  13185  fzsubel  13452  fzoval  13552  seqid3  13945  mulexp  14000  sqdiv  14020  hashdom  14278  hashun  14281  ccatfval  14472  splcl  14651  crim  15014  readd  15025  remullem  15027  imadd  15033  cjadd  15040  cjreim  15059  sqrtmul  15158  sqabsadd  15181  sqabssub  15182  absmul  15193  abs2dif  15232  bhmafibid1  15367  binom  15729  binomfallfac  15940  sinadd  16065  cosadd  16066  dvds2ln  16192  sadcaddlem  16360  bezoutlem4  16445  bezout  16446  absmulgcd  16452  gcddiv  16454  bezoutr1  16472  lcmgcd  16510  lcmfass  16549  nn0gcdsq  16655  crth  16681  pythagtriplem1  16720  pcqmul  16757  4sqlem4a  16855  4sqlem4  16856  prdsplusgval  17369  prdsmulrval  17371  prdsdsval  17374  prdsvscaval  17375  idmgmhm  18601  resmgmhm  18611  idmhm  18695  0mhm  18719  resmhm  18720  prdspjmhm  18729  pwsdiagmhm  18731  gsumws2  18742  frmdup1  18764  eqgval  19082  idghm  19136  resghm  19137  mulgmhm  19732  mulgghm  19733  srglmhm  20132  srgrmhm  20133  ringlghm  20223  ringrghm  20224  gsumdixp  20230  isrhm  20389  rhmval  20408  issrngd  20763  lmodvsghm  20849  pwssplit2  20987  xrsdsval  21340  expmhm  21366  expghm  21405  mulgghm2  21406  mulgrhm  21407  pzriprnglem4  21414  cygznlem3  21499  asclghm  21813  psrmulfval  21873  evlslem4  22004  mpfrcl  22013  mamuval  22301  mamufv  22302  mvmulval  22451  mndifsplit  22544  mat2pmatmul  22639  decpmatmul  22680  fmval  23851  fmf  23853  flffval  23897  divcnOLD  24777  divcn  24779  rescncf  24810  htpyco1  24897  tcphcph  25157  rrxdsfival  25333  ehl2eudisval  25343  volun  25466  dyadval  25513  dvlip  25918  ftc1a  25964  ftc2ditglem  25972  tdeglem3  25984  q1pval  26080  reefgim  26380  relogoprlem  26520  eflogeq  26531  zetacvg  26945  lgsdir2  27261  lgsdchr  27286  2sq2  27364  2sqnn0  27369  negsdi  27985  brbtwn2  28876  ax5seglem4  28903  axeuclid  28934  axcontlem2  28936  axcontlem4  28938  axcontlem8  28942  clwwlknccat  30033  ex-fpar  30432  ipasslem11  30810  hhssnv  31234  mayete3i  31698  idunop  31948  idhmop  31952  0lnfn  31955  lnopmi  31970  lnophsi  31971  lnopcoi  31973  hmops  31990  hmopm  31991  nlelshi  32030  cnlnadjlem2  32038  kbass6  32091  strlem3a  32222  hstrlem3a  32230  elrgspnlem2  33200  mndpluscn  33929  xrge0iifhom  33940  rezh  33972  probdsb  34425  resconn  35258  iscvm  35271  satfdmlem  35380  satffunlem1lem1  35414  satffunlem2lem1  35416  fwddifnval  36176  bj-bary1  37325  poimirlem15  37654  mbfposadd  37686  ftc1anclem3  37714  rrnmval  37847  dvhopaddN  41132  nnadddir  42282  cnreeu  42502  prjcrvfval  42643  pellex  42847  rmxfval  42916  rmyfval  42917  qirropth  42920  rmxycomplete  42929  jm2.15nn0  43015  rmxdioph  43028  expdiophlem2  43034  mendvsca  43199  deg1mhm  43212  mnringmulrvald  44239  addrval  44477  subrval  44478  fmulcl  45600  fmuldfeqlem1  45601  line  48743  itsclc0xyqsolr  48780