Theorem oveqan12d 7274

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539  (class class class)co 7255

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258

This theorem is referenced by:  oveqan12rd  7275  offval  7520  offval3  7798  odi  8372  omopth2  8377  oeoa  8390  ecovdi  8572  ackbij1lem9  9915  distrpi  10585  addpipq  10624  mulpipq  10627  lterpq  10657  reclem3pr  10736  1idsr  10785  mulcnsr  10823  mulid1  10904  1re  10906  mul02  11083  addcom  11091  mulsub  11348  mulsub2  11349  muleqadd  11549  divmuldiv  11605  div2sub  11730  addltmul  12139  xnegdi  12911  xadddilem  12957  fzsubel  13221  fzoval  13317  seqid3  13695  mulexp  13750  sqdiv  13769  hashdom  14022  hashun  14025  ccatfval  14204  splcl  14393  crim  14754  readd  14765  remullem  14767  imadd  14773  cjadd  14780  cjreim  14799  sqrtmul  14899  sqabsadd  14922  sqabssub  14923  absmul  14934  abs2dif  14972  bhmafibid1  15105  binom  15470  binomfallfac  15679  sinadd  15801  cosadd  15802  dvds2ln  15926  sadcaddlem  16092  bezoutlem4  16178  bezout  16179  absmulgcd  16185  gcddiv  16187  bezoutr1  16202  lcmgcd  16240  lcmfass  16279  nn0gcdsq  16384  crth  16407  pythagtriplem1  16445  pcqmul  16482  4sqlem4a  16580  4sqlem4  16581  prdsplusgval  17101  prdsmulrval  17103  prdsdsval  17106  prdsvscaval  17107  idmhm  18354  0mhm  18373  resmhm  18374  prdspjmhm  18382  pwsdiagmhm  18384  gsumws2  18396  frmdup1  18418  eqgval  18720  idghm  18764  resghm  18765  mulgmhm  19344  mulgghm  19345  srglmhm  19686  srgrmhm  19687  ringlghm  19758  ringrghm  19759  gsumdixp  19763  isrhm  19880  issrngd  20036  lmodvsghm  20099  pwssplit2  20237  xrsdsval  20554  expmhm  20579  expghm  20609  mulgghm2  20610  mulgrhm  20611  cygznlem3  20689  asclghm  20997  psrmulfval  21064  evlslem4  21194  mpfrcl  21205  mamuval  21445  mamufv  21446  mvmulval  21600  mndifsplit  21693  mat2pmatmul  21788  decpmatmul  21829  fmval  23002  fmf  23004  flffval  23048  divcn  23937  rescncf  23966  htpyco1  24047  tcphcph  24306  rrxdsfival  24482  ehl2eudisval  24492  volun  24614  dyadval  24661  dvlip  25062  ftc1a  25106  ftc2ditglem  25114  tdeglem3  25127  tdeglem3OLD  25128  q1pval  25223  reefgim  25514  relogoprlem  25651  eflogeq  25662  zetacvg  26069  lgsdir2  26383  lgsdchr  26408  2sq2  26486  2sqnn0  26491  brbtwn2  27176  ax5seglem4  27203  axeuclid  27234  axcontlem2  27236  axcontlem4  27238  axcontlem8  27242  clwwlknccat  28328  ex-fpar  28727  ipasslem11  29103  hhssnv  29527  mayete3i  29991  idunop  30241  idhmop  30245  0lnfn  30248  lnopmi  30263  lnophsi  30264  lnopcoi  30266  hmops  30283  hmopm  30284  nlelshi  30323  cnlnadjlem2  30331  kbass6  30384  strlem3a  30515  hstrlem3a  30523  mndpluscn  31778  xrge0iifhom  31789  rezh  31821  probdsb  32289  resconn  33108  iscvm  33121  satfdmlem  33230  satffunlem1lem1  33264  satffunlem2lem1  33266  fwddifnval  34392  bj-bary1  35410  poimirlem15  35719  mbfposadd  35751  ftc1anclem3  35779  rrnmval  35913  dvhopaddN  39055  nnadddir  40221  cnreeu  40359  pellex  40573  rmxfval  40642  rmyfval  40643  qirropth  40646  rmxycomplete  40655  jm2.15nn0  40741  rmxdioph  40754  expdiophlem2  40760  mendvsca  40932  deg1mhm  40948  mnringmulrvald  41734  addrval  41973  subrval  41974  fmulcl  43012  fmuldfeqlem1  43013  idmgmhm  45230  resmgmhm  45240  rhmval  45365  line  45966  itsclc0xyqsolr  46003