Theorem oveqan12d 7167

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1531  (class class class)co 7148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-rex 3142  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-iota 6307  df-fv 6356  df-ov 7151

This theorem is referenced by:  oveqan12rd  7168  offval  7408  offval3  7675  odi  8197  omopth2  8202  oeoa  8215  ecovdi  8397  ackbij1lem9  9642  distrpi  10312  addpipq  10351  mulpipq  10354  lterpq  10384  reclem3pr  10463  1idsr  10512  mulcnsr  10550  mulid1  10631  1re  10633  mul02  10810  addcom  10818  mulsub  11075  mulsub2  11076  muleqadd  11276  divmuldiv  11332  div2sub  11457  addltmul  11865  xnegdi  12633  xadddilem  12679  fzsubel  12935  fzoval  13031  seqid3  13406  mulexp  13460  sqdiv  13479  hashdom  13732  hashun  13735  ccatfval  13917  splcl  14106  crim  14466  readd  14477  remullem  14479  imadd  14485  cjadd  14492  cjreim  14511  sqrtmul  14611  sqabsadd  14634  sqabssub  14635  absmul  14646  abs2dif  14684  bhmafibid1  14817  binom  15177  binomfallfac  15387  sinadd  15509  cosadd  15510  dvds2ln  15634  sadcaddlem  15798  bezoutlem4  15882  bezout  15883  absmulgcd  15889  gcddiv  15891  bezoutr1  15905  lcmgcd  15943  lcmfass  15982  nn0gcdsq  16084  crth  16107  pythagtriplem1  16145  pcqmul  16182  4sqlem4a  16279  4sqlem4  16280  prdsplusgval  16738  prdsmulrval  16740  prdsdsval  16743  prdsvscaval  16744  idmhm  17957  0mhm  17976  resmhm  17977  prdspjmhm  17985  pwsdiagmhm  17987  gsumws2  17999  frmdup1  18021  eqgval  18321  idghm  18365  resghm  18366  mulgmhm  18940  mulgghm  18941  srglmhm  19277  srgrmhm  19278  ringlghm  19346  ringrghm  19347  gsumdixp  19351  isrhm  19465  issrngd  19624  lmodvsghm  19687  pwssplit2  19824  asclghm  20104  psrmulfval  20157  evlslem4  20280  mpfrcl  20290  xrsdsval  20581  expmhm  20606  expghm  20635  mulgghm2  20636  mulgrhm  20637  cygznlem3  20708  mamuval  20989  mamufv  20990  mvmulval  21144  mndifsplit  21237  mat2pmatmul  21331  decpmatmul  21372  fmval  22543  fmf  22545  flffval  22589  divcn  23468  rescncf  23497  htpyco1  23574  tcphcph  23832  rrxdsfival  24008  ehl2eudisval  24018  volun  24138  dyadval  24185  dvlip  24582  ftc1a  24626  ftc2ditglem  24634  tdeglem3  24645  q1pval  24739  reefgim  25030  relogoprlem  25166  eflogeq  25177  zetacvg  25584  lgsdir2  25898  lgsdchr  25923  2sq2  26001  2sqnn0  26006  brbtwn2  26683  ax5seglem4  26710  axeuclid  26741  axcontlem2  26743  axcontlem4  26745  axcontlem8  26749  clwwlknccat  27834  ex-fpar  28233  ipasslem11  28609  hhssnv  29033  mayete3i  29497  idunop  29747  idhmop  29751  0lnfn  29754  lnopmi  29769  lnophsi  29770  lnopcoi  29772  hmops  29789  hmopm  29790  nlelshi  29829  cnlnadjlem2  29837  kbass6  29890  strlem3a  30021  hstrlem3a  30029  mndpluscn  31162  xrge0iifhom  31173  rezh  31205  probdsb  31673  resconn  32486  iscvm  32499  satfdmlem  32608  satffunlem1lem1  32642  satffunlem2lem1  32644  fwddifnval  33617  bj-bary1  34585  poimirlem15  34899  mbfposadd  34931  ftc1anclem3  34961  rrnmval  35098  dvhopaddN  38242  nnadddir  39154  pellex  39423  rmxfval  39492  rmyfval  39493  qirropth  39496  rmxycomplete  39505  jm2.15nn0  39591  rmxdioph  39604  expdiophlem2  39610  mendvsca  39782  deg1mhm  39798  addrval  40789  subrval  40790  fmulcl  41852  fmuldfeqlem1  41853  idmgmhm  44046  resmgmhm  44056  rhmval  44181  line  44710  itsclc0xyqsolr  44747