Theorem oveqan12d 7026

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1520  (class class class)co 7007

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-ext 2767

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1080  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-rex 3109  df-rab 3112  df-v 3434  df-dif 3857  df-un 3859  df-in 3861  df-ss 3869  df-nul 4207  df-if 4376  df-sn 4467  df-pr 4469  df-op 4473  df-uni 4740  df-br 4957  df-iota 6181  df-fv 6225  df-ov 7010

This theorem is referenced by:  oveqan12rd  7027  offval  7265  offval3  7530  odi  8046  omopth2  8051  oeoa  8064  ecovdi  8246  ackbij1lem9  9485  distrpi  10155  addpipq  10194  mulpipq  10197  lterpq  10227  reclem3pr  10306  1idsr  10355  mulcnsr  10393  mulid1  10474  1re  10476  mul02  10654  addcom  10662  mulsub  10920  mulsub2  10921  muleqadd  11121  divmuldiv  11177  div2sub  11302  addltmul  11710  xnegdi  12480  xadddilem  12526  fzsubel  12782  fzoval  12878  seqid3  13252  mulexp  13306  sqdiv  13325  hashdom  13576  hashun  13579  ccatfval  13759  splcl  13938  crim  14296  readd  14307  remullem  14309  imadd  14315  cjadd  14322  cjreim  14341  sqrtmul  14441  sqabsadd  14464  sqabssub  14465  absmul  14476  abs2dif  14514  bhmafibid1  14647  binom  15006  binomfallfac  15216  sinadd  15338  cosadd  15339  dvds2ln  15463  sadcaddlem  15627  bezoutlem4  15707  bezout  15708  absmulgcd  15714  gcddiv  15716  bezoutr1  15730  lcmgcd  15768  lcmfass  15807  nn0gcdsq  15909  crth  15932  pythagtriplem1  15970  pcqmul  16007  4sqlem4a  16104  4sqlem4  16105  prdsplusgval  16563  prdsmulrval  16565  prdsdsval  16568  prdsvscaval  16569  idmhm  17771  0mhm  17785  resmhm  17786  prdspjmhm  17794  pwsdiagmhm  17796  gsumws2  17806  frmdup1  17828  eqgval  18070  idghm  18102  resghm  18103  mulgmhm  18661  mulgghm  18662  srglmhm  18963  srgrmhm  18964  ringlghm  19032  ringrghm  19033  gsumdixp  19037  isrhm  19151  issrngd  19310  lmodvsghm  19373  pwssplit2  19510  asclghm  19788  psrmulfval  19841  evlslem4  19963  mpfrcl  19973  xrsdsval  20259  expmhm  20284  expghm  20313  mulgghm2  20314  mulgrhm  20315  cygznlem3  20386  mamuval  20667  mamufv  20668  mvmulval  20824  mndifsplit  20917  mat2pmatmul  21011  decpmatmul  21052  fmval  22223  fmf  22225  flffval  22269  divcn  23147  rescncf  23176  htpyco1  23253  tcphcph  23511  rrxdsfival  23687  ehl2eudisval  23697  volun  23817  dyadval  23864  dvlip  24261  ftc1a  24305  ftc2ditglem  24313  tdeglem3  24324  q1pval  24418  reefgim  24709  relogoprlem  24843  eflogeq  24854  zetacvg  25262  lgsdir2  25576  lgsdchr  25601  2sq2  25679  2sqnn0  25684  brbtwn2  26362  ax5seglem4  26389  axeuclid  26420  axcontlem2  26422  axcontlem4  26424  axcontlem8  26428  clwwlknccat  27517  ipasslem11  28296  hhssnv  28720  mayete3i  29184  idunop  29434  idhmop  29438  0lnfn  29441  lnopmi  29456  lnophsi  29457  lnopcoi  29459  hmops  29476  hmopm  29477  nlelshi  29516  cnlnadjlem2  29524  kbass6  29577  strlem3a  29708  hstrlem3a  29716  mndpluscn  30742  xrge0iifhom  30753  rezh  30785  probdsb  31253  resconn  32057  iscvm  32070  satfdmlem  32177  satffunlem1lem1  32210  satffunlem2lem1  32212  fwddifnval  33178  bj-bary1  34076  poimirlem15  34384  mbfposadd  34416  ftc1anclem3  34446  rrnmval  34584  dvhopaddN  37731  pellex  38868  rmxfval  38937  rmyfval  38938  qirropth  38941  rmxycomplete  38950  jm2.15nn0  39036  rmxdioph  39049  expdiophlem2  39055  mendvsca  39227  deg1mhm  39243  addrval  40289  subrval  40290  fmulcl  41358  fmuldfeqlem1  41359  idmgmhm  43491  resmgmhm  43501  rhmval  43622  offval0  43999  line  44154  itsclc0xyqsolr  44191