Theorem oveqan12d 7383

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

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

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6452  df-fv 6504  df-ov 7367

This theorem is referenced by:  oveqan12rd  7384  offval  7637  offval3  7932  odi  8511  omopth2  8516  oeoa  8530  ecovdi  8769  ackbij1lem9  10146  distrpi  10818  addpipq  10857  mulpipq  10860  lterpq  10890  reclem3pr  10969  1idsr  11018  mulcnsr  11056  mulrid  11139  1re  11141  mul02  11321  addcom  11329  mulsub  11590  mulsub2  11591  muleqadd  11791  divmuldiv  11852  div2sub  11977  nnadddir  12230  addltmul  12410  xnegdi  13197  xadddilem  13243  fzsubel  13511  fzoval  13611  seqid3  14005  mulexp  14060  sqdiv  14080  hashdom  14338  hashun  14341  ccatfval  14532  splcl  14711  crim  15074  readd  15085  remullem  15087  imadd  15093  cjadd  15100  cjreim  15119  sqrtmul  15218  sqabsadd  15241  sqabssub  15242  absmul  15253  abs2dif  15292  bhmafibid1  15427  binom  15792  binomfallfac  16003  sinadd  16128  cosadd  16129  dvds2ln  16255  sadcaddlem  16423  bezoutlem4  16508  bezout  16509  absmulgcd  16515  gcddiv  16517  bezoutr1  16535  lcmgcd  16573  lcmfass  16612  nn0gcdsq  16719  crth  16745  pythagtriplem1  16784  pcqmul  16821  4sqlem4a  16919  4sqlem4  16920  prdsplusgval  17433  prdsmulrval  17435  prdsdsval  17438  prdsvscaval  17439  idmgmhm  18666  resmgmhm  18676  idmhm  18760  0mhm  18784  resmhm  18785  prdspjmhm  18794  pwsdiagmhm  18796  gsumws2  18807  frmdup1  18829  eqgval  19149  idghm  19203  resghm  19204  mulgmhm  19799  mulgghm  19800  srglmhm  20199  srgrmhm  20200  ringlghm  20290  ringrghm  20291  gsumdixp  20295  isrhm  20455  rhmval  20474  issrngd  20829  lmodvsghm  20915  pwssplit2  21052  xrsdsval  21388  expmhm  21413  expghm  21452  mulgghm2  21453  mulgrhm  21454  pzriprnglem4  21461  cygznlem3  21546  asclghm  21859  psrmulfval  21919  evlslem4  22051  mpfrcl  22060  mamuval  22355  mamufv  22356  mvmulval  22505  mndifsplit  22598  mat2pmatmul  22693  decpmatmul  22734  fmval  23905  fmf  23907  flffval  23951  divcn  24832  rescncf  24861  htpyco1  24942  tcphcph  25201  rrxdsfival  25377  ehl2eudisval  25387  volun  25509  dyadval  25556  dvlip  25957  ftc1a  26001  ftc2ditglem  26009  tdeglem3  26021  q1pval  26117  reefgim  26412  relogoprlem  26552  eflogeq  26563  zetacvg  26975  lgsdir2  27290  lgsdchr  27315  2sq2  27393  2sqnn0  27398  negsdi  28039  brbtwn2  28971  ax5seglem4  28998  axeuclid  29029  axcontlem2  29031  axcontlem4  29033  axcontlem8  29037  clwwlknccat  30130  ex-fpar  30529  ipasslem11  30908  hhssnv  31332  mayete3i  31796  idunop  32046  idhmop  32050  0lnfn  32053  lnopmi  32068  lnophsi  32069  lnopcoi  32071  hmops  32088  hmopm  32089  nlelshi  32128  cnlnadjlem2  32136  kbass6  32189  strlem3a  32320  hstrlem3a  32328  elrgspnlem2  33301  mndpluscn  34067  xrge0iifhom  34078  rezh  34110  probdsb  34563  resconn  35425  iscvm  35438  satfdmlem  35547  satffunlem1lem1  35581  satffunlem2lem1  35583  fwddifnval  36342  bj-bary1  37623  poimirlem15  37953  mbfposadd  37985  ftc1anclem3  38013  rrnmval  38146  dvhopaddN  41557  cnreeu  42932  prjcrvfval  43061  pellex  43260  rmxfval  43329  rmyfval  43330  qirropth  43333  rmxycomplete  43342  jm2.15nn0  43428  rmxdioph  43441  expdiophlem2  43447  mendvsca  43612  deg1mhm  43625  mnringmulrvald  44651  addrval  44889  subrval  44890  fmulcl  46008  fmuldfeqlem1  46009  line  49199  itsclc0xyqsolr  49236