Theorem oveqan12d 7430

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

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1539  (class class class)co 7411

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6494  df-fv 6550  df-ov 7414

This theorem is referenced by:  oveqan12rd  7431  offval  7681  offval3  7971  odi  8581  omopth2  8586  oeoa  8599  ecovdi  8821  ackbij1lem9  10225  distrpi  10895  addpipq  10934  mulpipq  10937  lterpq  10967  reclem3pr  11046  1idsr  11095  mulcnsr  11133  mulrid  11216  1re  11218  mul02  11396  addcom  11404  mulsub  11661  mulsub2  11662  muleqadd  11862  divmuldiv  11918  div2sub  12043  addltmul  12452  xnegdi  13231  xadddilem  13277  fzsubel  13541  fzoval  13637  seqid3  14016  mulexp  14071  sqdiv  14090  hashdom  14343  hashun  14346  ccatfval  14527  splcl  14706  crim  15066  readd  15077  remullem  15079  imadd  15085  cjadd  15092  cjreim  15111  sqrtmul  15210  sqabsadd  15233  sqabssub  15234  absmul  15245  abs2dif  15283  bhmafibid1  15416  binom  15780  binomfallfac  15989  sinadd  16111  cosadd  16112  dvds2ln  16236  sadcaddlem  16402  bezoutlem4  16488  bezout  16489  absmulgcd  16495  gcddiv  16497  bezoutr1  16510  lcmgcd  16548  lcmfass  16587  nn0gcdsq  16692  crth  16715  pythagtriplem1  16753  pcqmul  16790  4sqlem4a  16888  4sqlem4  16889  prdsplusgval  17423  prdsmulrval  17425  prdsdsval  17428  prdsvscaval  17429  idmgmhm  18626  resmgmhm  18636  idmhm  18717  0mhm  18736  resmhm  18737  prdspjmhm  18746  pwsdiagmhm  18748  gsumws2  18759  frmdup1  18781  eqgval  19093  idghm  19145  resghm  19146  mulgmhm  19736  mulgghm  19737  srglmhm  20115  srgrmhm  20116  ringlghm  20200  ringrghm  20201  gsumdixp  20207  isrhm  20369  rhmval  20391  issrngd  20612  lmodvsghm  20677  pwssplit2  20815  xrsdsval  21189  expmhm  21214  expghm  21246  mulgghm2  21247  mulgrhm  21248  pzriprnglem4  21253  cygznlem3  21344  asclghm  21656  psrmulfval  21723  evlslem4  21856  mpfrcl  21867  mamuval  22108  mamufv  22109  mvmulval  22265  mndifsplit  22358  mat2pmatmul  22453  decpmatmul  22494  fmval  23667  fmf  23669  flffval  23713  divcnOLD  24604  divcn  24606  rescncf  24637  htpyco1  24724  tcphcph  24985  rrxdsfival  25161  ehl2eudisval  25171  volun  25294  dyadval  25341  dvlip  25745  ftc1a  25789  ftc2ditglem  25797  tdeglem3  25810  tdeglem3OLD  25811  q1pval  25906  reefgim  26198  relogoprlem  26335  eflogeq  26346  zetacvg  26755  lgsdir2  27069  lgsdchr  27094  2sq2  27172  2sqnn0  27177  negsdi  27763  brbtwn2  28430  ax5seglem4  28457  axeuclid  28488  axcontlem2  28490  axcontlem4  28492  axcontlem8  28496  clwwlknccat  29583  ex-fpar  29982  ipasslem11  30360  hhssnv  30784  mayete3i  31248  idunop  31498  idhmop  31502  0lnfn  31505  lnopmi  31520  lnophsi  31521  lnopcoi  31523  hmops  31540  hmopm  31541  nlelshi  31580  cnlnadjlem2  31588  kbass6  31641  strlem3a  31772  hstrlem3a  31780  mndpluscn  33204  xrge0iifhom  33215  rezh  33249  probdsb  33719  resconn  34535  iscvm  34548  satfdmlem  34657  satffunlem1lem1  34691  satffunlem2lem1  34693  fwddifnval  35439  bj-bary1  36496  poimirlem15  36806  mbfposadd  36838  ftc1anclem3  36866  rrnmval  36999  dvhopaddN  40288  nnadddir  41486  cnreeu  41643  prjcrvfval  41675  pellex  41875  rmxfval  41944  rmyfval  41945  qirropth  41948  rmxycomplete  41958  jm2.15nn0  42044  rmxdioph  42057  expdiophlem2  42063  mendvsca  42235  deg1mhm  42251  mnringmulrvald  43288  addrval  43527  subrval  43528  fmulcl  44595  fmuldfeqlem1  44596  line  47505  itsclc0xyqsolr  47542