Theorem oveqan12d 7379

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

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

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 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6449  df-fv 6501  df-ov 7363

This theorem is referenced by:  oveqan12rd  7380  offval  7633  offval3  7928  odi  8508  omopth2  8513  oeoa  8527  ecovdi  8766  ackbij1lem9  10141  distrpi  10813  addpipq  10852  mulpipq  10855  lterpq  10885  reclem3pr  10964  1idsr  11013  mulcnsr  11051  mulrid  11134  1re  11136  mul02  11315  addcom  11323  mulsub  11584  mulsub2  11585  muleqadd  11785  divmuldiv  11845  div2sub  11970  addltmul  12381  xnegdi  13167  xadddilem  13213  fzsubel  13480  fzoval  13580  seqid3  13973  mulexp  14028  sqdiv  14048  hashdom  14306  hashun  14309  ccatfval  14500  splcl  14679  crim  15042  readd  15053  remullem  15055  imadd  15061  cjadd  15068  cjreim  15087  sqrtmul  15186  sqabsadd  15209  sqabssub  15210  absmul  15221  abs2dif  15260  bhmafibid1  15395  binom  15757  binomfallfac  15968  sinadd  16093  cosadd  16094  dvds2ln  16220  sadcaddlem  16388  bezoutlem4  16473  bezout  16474  absmulgcd  16480  gcddiv  16482  bezoutr1  16500  lcmgcd  16538  lcmfass  16577  nn0gcdsq  16683  crth  16709  pythagtriplem1  16748  pcqmul  16785  4sqlem4a  16883  4sqlem4  16884  prdsplusgval  17397  prdsmulrval  17399  prdsdsval  17402  prdsvscaval  17403  idmgmhm  18630  resmgmhm  18640  idmhm  18724  0mhm  18748  resmhm  18749  prdspjmhm  18758  pwsdiagmhm  18760  gsumws2  18771  frmdup1  18793  eqgval  19110  idghm  19164  resghm  19165  mulgmhm  19760  mulgghm  19761  srglmhm  20160  srgrmhm  20161  ringlghm  20251  ringrghm  20252  gsumdixp  20258  isrhm  20418  rhmval  20437  issrngd  20792  lmodvsghm  20878  pwssplit2  21016  xrsdsval  21369  expmhm  21395  expghm  21434  mulgghm2  21435  mulgrhm  21436  pzriprnglem4  21443  cygznlem3  21528  asclghm  21842  psrmulfval  21903  evlslem4  22035  mpfrcl  22044  mamuval  22341  mamufv  22342  mvmulval  22491  mndifsplit  22584  mat2pmatmul  22679  decpmatmul  22720  fmval  23891  fmf  23893  flffval  23937  divcnOLD  24817  divcn  24819  rescncf  24850  htpyco1  24937  tcphcph  25197  rrxdsfival  25373  ehl2eudisval  25383  volun  25506  dyadval  25553  dvlip  25958  ftc1a  26004  ftc2ditglem  26012  tdeglem3  26024  q1pval  26120  reefgim  26420  relogoprlem  26560  eflogeq  26571  zetacvg  26985  lgsdir2  27301  lgsdchr  27326  2sq2  27404  2sqnn0  27409  negsdi  28050  brbtwn2  28982  ax5seglem4  29009  axeuclid  29040  axcontlem2  29042  axcontlem4  29044  axcontlem8  29048  clwwlknccat  30142  ex-fpar  30541  ipasslem11  30919  hhssnv  31343  mayete3i  31807  idunop  32057  idhmop  32061  0lnfn  32064  lnopmi  32079  lnophsi  32080  lnopcoi  32082  hmops  32099  hmopm  32100  nlelshi  32139  cnlnadjlem2  32147  kbass6  32200  strlem3a  32331  hstrlem3a  32339  elrgspnlem2  33327  mndpluscn  34085  xrge0iifhom  34096  rezh  34128  probdsb  34581  resconn  35442  iscvm  35455  satfdmlem  35564  satffunlem1lem1  35598  satffunlem2lem1  35600  fwddifnval  36359  bj-bary1  37519  poimirlem15  37838  mbfposadd  37870  ftc1anclem3  37898  rrnmval  38031  dvhopaddN  41442  nnadddir  42592  cnreeu  42812  prjcrvfval  42941  pellex  43144  rmxfval  43213  rmyfval  43214  qirropth  43217  rmxycomplete  43226  jm2.15nn0  43312  rmxdioph  43325  expdiophlem2  43331  mendvsca  43496  deg1mhm  43509  mnringmulrvald  44535  addrval  44773  subrval  44774  fmulcl  45894  fmuldfeqlem1  45895  line  49045  itsclc0xyqsolr  49082