Theorem oveqan12d 7380

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

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

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 7364

This theorem is referenced by:  oveqan12rd  7381  offval  7634  offval3  7929  odi  8509  omopth2  8514  oeoa  8528  ecovdi  8767  ackbij1lem9  10142  distrpi  10814  addpipq  10853  mulpipq  10856  lterpq  10886  reclem3pr  10965  1idsr  11014  mulcnsr  11052  mulrid  11135  1re  11137  mul02  11316  addcom  11324  mulsub  11585  mulsub2  11586  muleqadd  11786  divmuldiv  11846  div2sub  11971  addltmul  12382  xnegdi  13168  xadddilem  13214  fzsubel  13481  fzoval  13581  seqid3  13974  mulexp  14029  sqdiv  14049  hashdom  14307  hashun  14310  ccatfval  14501  splcl  14680  crim  15043  readd  15054  remullem  15056  imadd  15062  cjadd  15069  cjreim  15088  sqrtmul  15187  sqabsadd  15210  sqabssub  15211  absmul  15222  abs2dif  15261  bhmafibid1  15396  binom  15758  binomfallfac  15969  sinadd  16094  cosadd  16095  dvds2ln  16221  sadcaddlem  16389  bezoutlem4  16474  bezout  16475  absmulgcd  16481  gcddiv  16483  bezoutr1  16501  lcmgcd  16539  lcmfass  16578  nn0gcdsq  16684  crth  16710  pythagtriplem1  16749  pcqmul  16786  4sqlem4a  16884  4sqlem4  16885  prdsplusgval  17398  prdsmulrval  17400  prdsdsval  17403  prdsvscaval  17404  idmgmhm  18631  resmgmhm  18641  idmhm  18725  0mhm  18749  resmhm  18750  prdspjmhm  18759  pwsdiagmhm  18761  gsumws2  18772  frmdup1  18794  eqgval  19111  idghm  19165  resghm  19166  mulgmhm  19761  mulgghm  19762  srglmhm  20161  srgrmhm  20162  ringlghm  20252  ringrghm  20253  gsumdixp  20259  isrhm  20419  rhmval  20438  issrngd  20793  lmodvsghm  20879  pwssplit2  21017  xrsdsval  21370  expmhm  21396  expghm  21435  mulgghm2  21436  mulgrhm  21437  pzriprnglem4  21444  cygznlem3  21529  asclghm  21843  psrmulfval  21904  evlslem4  22036  mpfrcl  22045  mamuval  22342  mamufv  22343  mvmulval  22492  mndifsplit  22585  mat2pmatmul  22680  decpmatmul  22721  fmval  23892  fmf  23894  flffval  23938  divcnOLD  24818  divcn  24820  rescncf  24851  htpyco1  24938  tcphcph  25198  rrxdsfival  25374  ehl2eudisval  25384  volun  25507  dyadval  25554  dvlip  25959  ftc1a  26005  ftc2ditglem  26013  tdeglem3  26025  q1pval  26121  reefgim  26421  relogoprlem  26561  eflogeq  26572  zetacvg  26986  lgsdir2  27302  lgsdchr  27327  2sq2  27405  2sqnn0  27410  negsdi  28051  brbtwn2  28983  ax5seglem4  29010  axeuclid  29041  axcontlem2  29043  axcontlem4  29045  axcontlem8  29049  clwwlknccat  30143  ex-fpar  30542  ipasslem11  30920  hhssnv  31344  mayete3i  31808  idunop  32058  idhmop  32062  0lnfn  32065  lnopmi  32080  lnophsi  32081  lnopcoi  32083  hmops  32100  hmopm  32101  nlelshi  32140  cnlnadjlem2  32148  kbass6  32201  strlem3a  32332  hstrlem3a  32340  elrgspnlem2  33329  mndpluscn  34096  xrge0iifhom  34107  rezh  34139  probdsb  34592  resconn  35453  iscvm  35466  satfdmlem  35575  satffunlem1lem1  35609  satffunlem2lem1  35611  fwddifnval  36370  bj-bary1  37530  poimirlem15  37849  mbfposadd  37881  ftc1anclem3  37909  rrnmval  38042  dvhopaddN  41453  nnadddir  42603  cnreeu  42823  prjcrvfval  42952  pellex  43155  rmxfval  43224  rmyfval  43225  qirropth  43228  rmxycomplete  43237  jm2.15nn0  43323  rmxdioph  43336  expdiophlem2  43342  mendvsca  43507  deg1mhm  43520  mnringmulrvald  44546  addrval  44784  subrval  44785  fmulcl  45904  fmuldfeqlem1  45905  line  49055  itsclc0xyqsolr  49092