Theorem oveqan12d 7439

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569  (class class class)co 7420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423

This theorem is used by:  oveqan12rd  7440  offval  7702  offval3  7994  odi  8587  omopth2  8592  oeoa  8606  ecovdi  8846  ackbij1lem9  10305  distrpi  10983  addpipq  11022  mulpipq  11025  lterpq  11055  reclem3pr  11134  1idsr  11183  mulcnsr  11221  mulrid  11306  1re  11308  mul02  11488  addcom  11496  mulsub  11759  mulsub2  11760  muleqadd  11960  divmuldiv  12017  div2sub  12142  nnadddir  12394  addltmul  12582  xnegdi  13378  xadddilem  13424  fzsubel  13694  fzoval  13794  seqid3  14189  mulexp  14244  sqdiv  14264  hashdom  14523  hashun  14526  ccatfval  14718  splcl  14901  crim  15282  readd  15293  remullem  15295  imadd  15301  cjadd  15308  cjreim  15327  sqrtmul  15426  sqabsadd  15449  sqabssub  15450  absmul  15461  abs2dif  15500  bhmafibid1  15635  binom  15999  binomfallfac  16207  sinadd  16332  cosadd  16333  dvds2ln  16459  sadcaddlem  16627  bezoutlem4  16715  bezout  16716  absmulgcd  16722  gcddiv  16724  bezoutr1  16744  lcmgcd  16782  lcmfass  16821  nn0gcdsq  16928  crth  16955  pythagtriplem1  16994  pcqmul  17031  4sqlem4a  17129  4sqlem4  17130  prdsplusgval  17644  prdsmulrval  17646  prdsdsval  17649  prdsvscaval  17650  idmgmhm  18890  resmgmhm  18900  idmhm  18990  0mhm  19015  resmhm  19016  prdspjmhm  19025  pwsdiagmhm  19027  gsumws2  19038  frmdup1  19060  eqgval  19389  idghm  19445  resghm  19446  mulgmhm  20041  mulgghm  20042  srglmhm  20447  srgrmhm  20448  ringlghm  20543  ringrghm  20544  gsumdixp  20548  isrhm  20709  rhmval  20738  issrngd  21112  lmodvsghm  21198  pwssplit2  21335  xrsdsval  21717  expmhm  21742  expghm  21781  mulgghm2  21782  mulgrhm  21783  pzriprnglem4  21790  cygznlem3  21875  asclghm  22190  psrmulfval  22251  evlslem4  22385  mpfrcl  22394  mamuval  22708  mamufv  22709  mvmulval  22858  mndifsplit  22951  mat2pmatmul  23049  decpmatmul  23090  fmval  24262  fmf  24264  flffval  24308  divcn  25189  rescncf  25218  htpyco1  25299  tcphcph  25558  rrxdsfival  25734  ehl2eudisval  25744  volun  25866  dyadval  25913  dvlip  26313  ftc1a  26357  ftc2ditglem  26365  tdeglem3  26377  q1pval  26473  reefgim  26777  relogoprlem  26919  eflogeq  26930  zetacvg  27342  lgsdir2  27657  lgsdchr  27682  2sq2  27760  2sqnn0  27765  negsdi  28436  brbtwn2  29483  ax5seglem4  29510  axeuclid  29541  axcontlem2  29543  axcontlem4  29545  axcontlem8  29549  clwwlknccat  30654  ex-fpar  31063  ipasslem11  31442  hhssnv  31866  mayete3i  32330  idunop  32580  idhmop  32584  0lnfn  32587  lnopmi  32602  lnophsi  32603  lnopcoi  32605  hmops  32622  hmopm  32623  nlelshi  32662  cnlnadjlem2  32670  kbass6  32723  strlem3a  32854  hstrlem3a  32862  elrgspnlem2  33846  mndpluscn  34600  xrge0iifhom  34611  rezh  34643  probdsb  35096  resconn  36053  iscvm  36066  satfdmlem  36175  satffunlem1lem1  36209  satffunlem2lem1  36211  fwddifnval  36970  bj-bary1  38276  poimirlem15  38596  mbfposadd  38628  ftc1anclem3  38656  rrnmval  38805  dvhopaddN  42214  cnreeu  43597  prjcrvfval  43710  pellex  43885  rmxfval  43954  rmyfval  43955  qirropth  43958  rmxycomplete  43967  jm2.15nn0  44053  rmxdioph  44066  expdiophlem2  44072  mendvsca  44232  deg1mhm  44245  mnringmulrvald  45268  addrval  45491  subrval  45492  hashnna  46052  fmulcl  46636  fmuldfeqlem1  46637  line  49887  itsclc0xyqsolr  49924