Theorem oveqan12d 7427

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570  (class class class)co 7408

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-iota 6483  df-fv 6535  df-ov 7411

This theorem is used by:  oveqan12rd  7428  offval  7685  offval3  7977  odi  8565  omopth2  8570  oeoa  8584  ecovdi  8824  ackbij1lem9  10276  distrpi  10954  addpipq  10993  mulpipq  10996  lterpq  11026  reclem3pr  11105  1idsr  11154  mulcnsr  11192  mulrid  11277  1re  11279  mul02  11459  addcom  11467  mulsub  11728  mulsub2  11729  muleqadd  11929  divmuldiv  11986  div2sub  12111  nnadddir  12363  addltmul  12551  xnegdi  13347  xadddilem  13393  fzsubel  13662  fzoval  13762  seqid3  14157  mulexp  14212  sqdiv  14232  hashdom  14490  hashun  14493  ccatfval  14685  splcl  14868  crim  15249  readd  15260  remullem  15262  imadd  15268  cjadd  15275  cjreim  15294  sqrtmul  15393  sqabsadd  15416  sqabssub  15417  absmul  15428  abs2dif  15467  bhmafibid1  15602  binom  15966  binomfallfac  16174  sinadd  16299  cosadd  16300  dvds2ln  16426  sadcaddlem  16594  bezoutlem4  16679  bezout  16680  absmulgcd  16686  gcddiv  16688  bezoutr1  16706  lcmgcd  16744  lcmfass  16783  nn0gcdsq  16890  crth  16916  pythagtriplem1  16955  pcqmul  16992  4sqlem4a  17090  4sqlem4  17091  prdsplusgval  17605  prdsmulrval  17607  prdsdsval  17610  prdsvscaval  17611  idmgmhm  18851  resmgmhm  18861  idmhm  18951  0mhm  18976  resmhm  18977  prdspjmhm  18986  pwsdiagmhm  18988  gsumws2  18999  frmdup1  19021  eqgval  19350  idghm  19406  resghm  19407  mulgmhm  20002  mulgghm  20003  srglmhm  20408  srgrmhm  20409  ringlghm  20504  ringrghm  20505  gsumdixp  20509  isrhm  20670  rhmval  20699  issrngd  21073  lmodvsghm  21159  pwssplit2  21296  xrsdsval  21678  expmhm  21703  expghm  21742  mulgghm2  21743  mulgrhm  21744  pzriprnglem4  21751  cygznlem3  21836  asclghm  22151  psrmulfval  22212  evlslem4  22346  mpfrcl  22355  mamuval  22669  mamufv  22670  mvmulval  22819  mndifsplit  22912  mat2pmatmul  23010  decpmatmul  23051  fmval  24223  fmf  24225  flffval  24269  divcn  25150  rescncf  25179  htpyco1  25260  tcphcph  25519  rrxdsfival  25695  ehl2eudisval  25705  volun  25827  dyadval  25874  dvlip  26274  ftc1a  26318  ftc2ditglem  26326  tdeglem3  26338  q1pval  26434  reefgim  26740  relogoprlem  26882  eflogeq  26893  zetacvg  27305  lgsdir2  27620  lgsdchr  27645  2sq2  27723  2sqnn0  27728  negsdi  28369  brbtwn2  29416  ax5seglem4  29443  axeuclid  29474  axcontlem2  29476  axcontlem4  29478  axcontlem8  29482  clwwlknccat  30587  ex-fpar  30996  ipasslem11  31375  hhssnv  31799  mayete3i  32263  idunop  32513  idhmop  32517  0lnfn  32520  lnopmi  32535  lnophsi  32536  lnopcoi  32538  hmops  32555  hmopm  32556  nlelshi  32595  cnlnadjlem2  32603  kbass6  32656  strlem3a  32787  hstrlem3a  32795  elrgspnlem2  33737  mndpluscn  34491  xrge0iifhom  34502  rezh  34534  probdsb  34988  resconn  35932  iscvm  35945  satfdmlem  36054  satffunlem1lem1  36088  satffunlem2lem1  36090  fwddifnval  36850  bj-bary1  38153  poimirlem15  38473  mbfposadd  38505  ftc1anclem3  38533  rrnmval  38682  dvhopaddN  42091  cnreeu  43482  prjcrvfval  43581  pellex  43780  rmxfval  43849  rmyfval  43850  qirropth  43853  rmxycomplete  43862  jm2.15nn0  43948  rmxdioph  43961  expdiophlem2  43967  mendvsca  44132  deg1mhm  44145  mnringmulrvald  45169  addrval  45392  subrval  45393  hashnna  45946  fmulcl  46515  fmuldfeqlem1  46516  line  49766  itsclc0xyqsolr  49803