Theorem oveqan12d 7406

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  (class class class)co 7387

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390

This theorem is referenced by:  oveqan12rd  7407  offval  7662  offval3  7961  odi  8543  omopth2  8548  oeoa  8561  ecovdi  8798  ackbij1lem9  10180  distrpi  10851  addpipq  10890  mulpipq  10893  lterpq  10923  reclem3pr  11002  1idsr  11051  mulcnsr  11089  mulrid  11172  1re  11174  mul02  11352  addcom  11360  mulsub  11621  mulsub2  11622  muleqadd  11822  divmuldiv  11882  div2sub  12007  addltmul  12418  xnegdi  13208  xadddilem  13254  fzsubel  13521  fzoval  13621  seqid3  14011  mulexp  14066  sqdiv  14086  hashdom  14344  hashun  14347  ccatfval  14538  splcl  14717  crim  15081  readd  15092  remullem  15094  imadd  15100  cjadd  15107  cjreim  15126  sqrtmul  15225  sqabsadd  15248  sqabssub  15249  absmul  15260  abs2dif  15299  bhmafibid1  15434  binom  15796  binomfallfac  16007  sinadd  16132  cosadd  16133  dvds2ln  16259  sadcaddlem  16427  bezoutlem4  16512  bezout  16513  absmulgcd  16519  gcddiv  16521  bezoutr1  16539  lcmgcd  16577  lcmfass  16616  nn0gcdsq  16722  crth  16748  pythagtriplem1  16787  pcqmul  16824  4sqlem4a  16922  4sqlem4  16923  prdsplusgval  17436  prdsmulrval  17438  prdsdsval  17441  prdsvscaval  17442  idmgmhm  18628  resmgmhm  18638  idmhm  18722  0mhm  18746  resmhm  18747  prdspjmhm  18756  pwsdiagmhm  18758  gsumws2  18769  frmdup1  18791  eqgval  19109  idghm  19163  resghm  19164  mulgmhm  19757  mulgghm  19758  srglmhm  20130  srgrmhm  20131  ringlghm  20221  ringrghm  20222  gsumdixp  20228  isrhm  20387  rhmval  20409  issrngd  20764  lmodvsghm  20829  pwssplit2  20967  xrsdsval  21327  expmhm  21353  expghm  21385  mulgghm2  21386  mulgrhm  21387  pzriprnglem4  21394  cygznlem3  21479  asclghm  21792  psrmulfval  21852  evlslem4  21983  mpfrcl  21992  mamuval  22280  mamufv  22281  mvmulval  22430  mndifsplit  22523  mat2pmatmul  22618  decpmatmul  22659  fmval  23830  fmf  23832  flffval  23876  divcnOLD  24757  divcn  24759  rescncf  24790  htpyco1  24877  tcphcph  25137  rrxdsfival  25313  ehl2eudisval  25323  volun  25446  dyadval  25493  dvlip  25898  ftc1a  25944  ftc2ditglem  25952  tdeglem3  25964  q1pval  26060  reefgim  26360  relogoprlem  26500  eflogeq  26511  zetacvg  26925  lgsdir2  27241  lgsdchr  27266  2sq2  27344  2sqnn0  27349  negsdi  27956  brbtwn2  28832  ax5seglem4  28859  axeuclid  28890  axcontlem2  28892  axcontlem4  28894  axcontlem8  28898  clwwlknccat  29992  ex-fpar  30391  ipasslem11  30769  hhssnv  31193  mayete3i  31657  idunop  31907  idhmop  31911  0lnfn  31914  lnopmi  31929  lnophsi  31930  lnopcoi  31932  hmops  31949  hmopm  31950  nlelshi  31989  cnlnadjlem2  31997  kbass6  32050  strlem3a  32181  hstrlem3a  32189  elrgspnlem2  33194  mndpluscn  33916  xrge0iifhom  33927  rezh  33959  probdsb  34413  resconn  35233  iscvm  35246  satfdmlem  35355  satffunlem1lem1  35389  satffunlem2lem1  35391  fwddifnval  36151  bj-bary1  37300  poimirlem15  37629  mbfposadd  37661  ftc1anclem3  37689  rrnmval  37822  dvhopaddN  41108  nnadddir  42258  cnreeu  42478  prjcrvfval  42619  pellex  42823  rmxfval  42892  rmyfval  42893  qirropth  42896  rmxycomplete  42906  jm2.15nn0  42992  rmxdioph  43005  expdiophlem2  43011  mendvsca  43176  deg1mhm  43189  mnringmulrvald  44216  addrval  44455  subrval  44456  fmulcl  45579  fmuldfeqlem1  45580  line  48721  itsclc0xyqsolr  48758