Theorem oveqan12d 7377

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

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

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6446  df-fv 6498  df-ov 7361

This theorem is referenced by:  oveqan12rd  7378  offval  7631  offval3  7926  odi  8505  omopth2  8510  oeoa  8524  ecovdi  8763  ackbij1lem9  10138  distrpi  10810  addpipq  10849  mulpipq  10852  lterpq  10882  reclem3pr  10961  1idsr  11010  mulcnsr  11048  mulrid  11131  1re  11133  mul02  11312  addcom  11320  mulsub  11581  mulsub2  11582  muleqadd  11782  divmuldiv  11842  div2sub  11967  addltmul  12378  xnegdi  13164  xadddilem  13210  fzsubel  13477  fzoval  13577  seqid3  13970  mulexp  14025  sqdiv  14045  hashdom  14303  hashun  14306  ccatfval  14497  splcl  14676  crim  15039  readd  15050  remullem  15052  imadd  15058  cjadd  15065  cjreim  15084  sqrtmul  15183  sqabsadd  15206  sqabssub  15207  absmul  15218  abs2dif  15257  bhmafibid1  15392  binom  15754  binomfallfac  15965  sinadd  16090  cosadd  16091  dvds2ln  16217  sadcaddlem  16385  bezoutlem4  16470  bezout  16471  absmulgcd  16477  gcddiv  16479  bezoutr1  16497  lcmgcd  16535  lcmfass  16574  nn0gcdsq  16680  crth  16706  pythagtriplem1  16745  pcqmul  16782  4sqlem4a  16880  4sqlem4  16881  prdsplusgval  17394  prdsmulrval  17396  prdsdsval  17399  prdsvscaval  17400  idmgmhm  18627  resmgmhm  18637  idmhm  18721  0mhm  18745  resmhm  18746  prdspjmhm  18755  pwsdiagmhm  18757  gsumws2  18768  frmdup1  18790  eqgval  19110  idghm  19164  resghm  19165  mulgmhm  19760  mulgghm  19761  srglmhm  20160  srgrmhm  20161  ringlghm  20251  ringrghm  20252  gsumdixp  20256  isrhm  20416  rhmval  20435  issrngd  20790  lmodvsghm  20876  pwssplit2  21014  xrsdsval  21367  expmhm  21393  expghm  21432  mulgghm2  21433  mulgrhm  21434  pzriprnglem4  21441  cygznlem3  21526  asclghm  21839  psrmulfval  21900  evlslem4  22032  mpfrcl  22041  mamuval  22336  mamufv  22337  mvmulval  22486  mndifsplit  22579  mat2pmatmul  22674  decpmatmul  22715  fmval  23886  fmf  23888  flffval  23932  divcn  24813  rescncf  24842  htpyco1  24923  tcphcph  25182  rrxdsfival  25358  ehl2eudisval  25368  volun  25490  dyadval  25537  dvlip  25939  ftc1a  25985  ftc2ditglem  25993  tdeglem3  26005  q1pval  26101  reefgim  26400  relogoprlem  26540  eflogeq  26551  zetacvg  26965  lgsdir2  27281  lgsdchr  27306  2sq2  27384  2sqnn0  27389  negsdi  28030  brbtwn2  28962  ax5seglem4  28989  axeuclid  29020  axcontlem2  29022  axcontlem4  29024  axcontlem8  29028  clwwlknccat  30122  ex-fpar  30521  ipasslem11  30900  hhssnv  31324  mayete3i  31788  idunop  32038  idhmop  32042  0lnfn  32045  lnopmi  32060  lnophsi  32061  lnopcoi  32063  hmops  32080  hmopm  32081  nlelshi  32120  cnlnadjlem2  32128  kbass6  32181  strlem3a  32312  hstrlem3a  32320  elrgspnlem2  33309  mndpluscn  34076  xrge0iifhom  34087  rezh  34119  probdsb  34572  resconn  35434  iscvm  35447  satfdmlem  35556  satffunlem1lem1  35590  satffunlem2lem1  35592  fwddifnval  36351  bj-bary1  37624  poimirlem15  37947  mbfposadd  37979  ftc1anclem3  38007  rrnmval  38140  dvhopaddN  41551  nnadddir  42701  cnreeu  42934  prjcrvfval  43063  pellex  43266  rmxfval  43335  rmyfval  43336  qirropth  43339  rmxycomplete  43348  jm2.15nn0  43434  rmxdioph  43447  expdiophlem2  43453  mendvsca  43618  deg1mhm  43631  mnringmulrvald  44657  addrval  44895  subrval  44896  fmulcl  46015  fmuldfeqlem1  46016  line  49166  itsclc0xyqsolr  49203