Theorem oveqan12d 7425

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542  (class class class)co 7406

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6493  df-fv 6549  df-ov 7409

This theorem is referenced by:  oveqan12rd  7426  offval  7676  offval3  7966  odi  8576  omopth2  8581  oeoa  8594  ecovdi  8816  ackbij1lem9  10220  distrpi  10890  addpipq  10929  mulpipq  10932  lterpq  10962  reclem3pr  11041  1idsr  11090  mulcnsr  11128  mulrid  11209  1re  11211  mul02  11389  addcom  11397  mulsub  11654  mulsub2  11655  muleqadd  11855  divmuldiv  11911  div2sub  12036  addltmul  12445  xnegdi  13224  xadddilem  13270  fzsubel  13534  fzoval  13630  seqid3  14009  mulexp  14064  sqdiv  14083  hashdom  14336  hashun  14339  ccatfval  14520  splcl  14699  crim  15059  readd  15070  remullem  15072  imadd  15078  cjadd  15085  cjreim  15104  sqrtmul  15203  sqabsadd  15226  sqabssub  15227  absmul  15238  abs2dif  15276  bhmafibid1  15409  binom  15773  binomfallfac  15982  sinadd  16104  cosadd  16105  dvds2ln  16229  sadcaddlem  16395  bezoutlem4  16481  bezout  16482  absmulgcd  16488  gcddiv  16490  bezoutr1  16503  lcmgcd  16541  lcmfass  16580  nn0gcdsq  16685  crth  16708  pythagtriplem1  16746  pcqmul  16783  4sqlem4a  16881  4sqlem4  16882  prdsplusgval  17416  prdsmulrval  17418  prdsdsval  17421  prdsvscaval  17422  idmhm  18678  0mhm  18697  resmhm  18698  prdspjmhm  18707  pwsdiagmhm  18709  gsumws2  18720  frmdup1  18742  eqgval  19052  idghm  19102  resghm  19103  mulgmhm  19690  mulgghm  19691  srglmhm  20038  srgrmhm  20039  ringlghm  20118  ringrghm  20119  gsumdixp  20125  isrhm  20250  issrngd  20462  lmodvsghm  20526  pwssplit2  20664  xrsdsval  20982  expmhm  21007  expghm  21037  mulgghm2  21038  mulgrhm  21039  cygznlem3  21117  asclghm  21429  psrmulfval  21496  evlslem4  21629  mpfrcl  21640  mamuval  21880  mamufv  21881  mvmulval  22037  mndifsplit  22130  mat2pmatmul  22225  decpmatmul  22266  fmval  23439  fmf  23441  flffval  23485  divcn  24376  rescncf  24405  htpyco1  24486  tcphcph  24746  rrxdsfival  24922  ehl2eudisval  24932  volun  25054  dyadval  25101  dvlip  25502  ftc1a  25546  ftc2ditglem  25554  tdeglem3  25567  tdeglem3OLD  25568  q1pval  25663  reefgim  25954  relogoprlem  26091  eflogeq  26102  zetacvg  26509  lgsdir2  26823  lgsdchr  26848  2sq2  26926  2sqnn0  26931  negsdi  27514  brbtwn2  28153  ax5seglem4  28180  axeuclid  28211  axcontlem2  28213  axcontlem4  28215  axcontlem8  28219  clwwlknccat  29306  ex-fpar  29705  ipasslem11  30081  hhssnv  30505  mayete3i  30969  idunop  31219  idhmop  31223  0lnfn  31226  lnopmi  31241  lnophsi  31242  lnopcoi  31244  hmops  31261  hmopm  31262  nlelshi  31301  cnlnadjlem2  31309  kbass6  31362  strlem3a  31493  hstrlem3a  31501  mndpluscn  32895  xrge0iifhom  32906  rezh  32940  probdsb  33410  resconn  34226  iscvm  34239  satfdmlem  34348  satffunlem1lem1  34382  satffunlem2lem1  34384  fwddifnval  35124  gg-divcn  35152  bj-bary1  36182  poimirlem15  36492  mbfposadd  36524  ftc1anclem3  36552  rrnmval  36685  dvhopaddN  39974  nnadddir  41182  cnreeu  41338  prjcrvfval  41370  pellex  41559  rmxfval  41628  rmyfval  41629  qirropth  41632  rmxycomplete  41642  jm2.15nn0  41728  rmxdioph  41741  expdiophlem2  41747  mendvsca  41919  deg1mhm  41935  mnringmulrvald  42972  addrval  43211  subrval  43212  fmulcl  44284  fmuldfeqlem1  44285  idmgmhm  46545  resmgmhm  46555  rhmval  46707  line  47372  itsclc0xyqsolr  47409