Theorem oveqan12d 7348

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1540  (class class class)co 7329

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3404  df-v 3443  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4269  df-if 4473  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4852  df-br 5090  df-iota 6425  df-fv 6481  df-ov 7332

This theorem is referenced by:  oveqan12rd  7349  offval  7596  offval3  7885  odi  8473  omopth2  8478  oeoa  8491  ecovdi  8677  ackbij1lem9  10077  distrpi  10747  addpipq  10786  mulpipq  10789  lterpq  10819  reclem3pr  10898  1idsr  10947  mulcnsr  10985  mulid1  11066  1re  11068  mul02  11246  addcom  11254  mulsub  11511  mulsub2  11512  muleqadd  11712  divmuldiv  11768  div2sub  11893  addltmul  12302  xnegdi  13075  xadddilem  13121  fzsubel  13385  fzoval  13481  seqid3  13860  mulexp  13915  sqdiv  13934  hashdom  14186  hashun  14189  ccatfval  14368  splcl  14555  crim  14917  readd  14928  remullem  14930  imadd  14936  cjadd  14943  cjreim  14962  sqrtmul  15062  sqabsadd  15085  sqabssub  15086  absmul  15097  abs2dif  15135  bhmafibid1  15268  binom  15633  binomfallfac  15842  sinadd  15964  cosadd  15965  dvds2ln  16089  sadcaddlem  16255  bezoutlem4  16341  bezout  16342  absmulgcd  16348  gcddiv  16350  bezoutr1  16363  lcmgcd  16401  lcmfass  16440  nn0gcdsq  16545  crth  16568  pythagtriplem1  16606  pcqmul  16643  4sqlem4a  16741  4sqlem4  16742  prdsplusgval  17273  prdsmulrval  17275  prdsdsval  17278  prdsvscaval  17279  idmhm  18528  0mhm  18547  resmhm  18548  prdspjmhm  18556  pwsdiagmhm  18558  gsumws2  18569  frmdup1  18591  eqgval  18893  idghm  18937  resghm  18938  mulgmhm  19516  mulgghm  19517  srglmhm  19858  srgrmhm  19859  ringlghm  19930  ringrghm  19931  gsumdixp  19935  isrhm  20052  issrngd  20219  lmodvsghm  20282  pwssplit2  20420  xrsdsval  20740  expmhm  20765  expghm  20795  mulgghm2  20796  mulgrhm  20797  cygznlem3  20875  asclghm  21185  psrmulfval  21252  evlslem4  21382  mpfrcl  21393  mamuval  21633  mamufv  21634  mvmulval  21790  mndifsplit  21883  mat2pmatmul  21978  decpmatmul  22019  fmval  23192  fmf  23194  flffval  23238  divcn  24129  rescncf  24158  htpyco1  24239  tcphcph  24499  rrxdsfival  24675  ehl2eudisval  24685  volun  24807  dyadval  24854  dvlip  25255  ftc1a  25299  ftc2ditglem  25307  tdeglem3  25320  tdeglem3OLD  25321  q1pval  25416  reefgim  25707  relogoprlem  25844  eflogeq  25855  zetacvg  26262  lgsdir2  26576  lgsdchr  26601  2sq2  26679  2sqnn0  26684  brbtwn2  27503  ax5seglem4  27530  axeuclid  27561  axcontlem2  27563  axcontlem4  27565  axcontlem8  27569  clwwlknccat  28656  ex-fpar  29055  ipasslem11  29431  hhssnv  29855  mayete3i  30319  idunop  30569  idhmop  30573  0lnfn  30576  lnopmi  30591  lnophsi  30592  lnopcoi  30594  hmops  30611  hmopm  30612  nlelshi  30651  cnlnadjlem2  30659  kbass6  30712  strlem3a  30843  hstrlem3a  30851  mndpluscn  32115  xrge0iifhom  32126  rezh  32160  probdsb  32630  resconn  33448  iscvm  33461  satfdmlem  33570  satffunlem1lem1  33604  satffunlem2lem1  33606  fwddifnval  34556  bj-bary1  35581  poimirlem15  35890  mbfposadd  35922  ftc1anclem3  35950  rrnmval  36084  dvhopaddN  39375  nnadddir  40550  cnreeu  40688  prjcrvfval  40718  pellex  40907  rmxfval  40976  rmyfval  40977  qirropth  40980  rmxycomplete  40990  jm2.15nn0  41076  rmxdioph  41089  expdiophlem2  41095  mendvsca  41267  deg1mhm  41283  mnringmulrvald  42155  addrval  42394  subrval  42395  fmulcl  43447  fmuldfeqlem1  43448  idmgmhm  45682  resmgmhm  45692  rhmval  45817  line  46418  itsclc0xyqsolr  46455