Theorem oveqan12d 7450

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  (class class class)co 7431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434

This theorem is referenced by:  oveqan12rd  7451  offval  7706  offval3  8007  odi  8617  omopth2  8622  oeoa  8635  ecovdi  8865  ackbij1lem9  10267  distrpi  10938  addpipq  10977  mulpipq  10980  lterpq  11010  reclem3pr  11089  1idsr  11138  mulcnsr  11176  mulrid  11259  1re  11261  mul02  11439  addcom  11447  mulsub  11706  mulsub2  11707  muleqadd  11907  divmuldiv  11967  div2sub  12092  addltmul  12502  xnegdi  13290  xadddilem  13336  fzsubel  13600  fzoval  13700  seqid3  14087  mulexp  14142  sqdiv  14161  hashdom  14418  hashun  14421  ccatfval  14611  splcl  14790  crim  15154  readd  15165  remullem  15167  imadd  15173  cjadd  15180  cjreim  15199  sqrtmul  15298  sqabsadd  15321  sqabssub  15322  absmul  15333  abs2dif  15371  bhmafibid1  15504  binom  15866  binomfallfac  16077  sinadd  16200  cosadd  16201  dvds2ln  16326  sadcaddlem  16494  bezoutlem4  16579  bezout  16580  absmulgcd  16586  gcddiv  16588  bezoutr1  16606  lcmgcd  16644  lcmfass  16683  nn0gcdsq  16789  crth  16815  pythagtriplem1  16854  pcqmul  16891  4sqlem4a  16989  4sqlem4  16990  prdsplusgval  17518  prdsmulrval  17520  prdsdsval  17523  prdsvscaval  17524  idmgmhm  18714  resmgmhm  18724  idmhm  18808  0mhm  18832  resmhm  18833  prdspjmhm  18842  pwsdiagmhm  18844  gsumws2  18855  frmdup1  18877  eqgval  19195  idghm  19249  resghm  19250  mulgmhm  19845  mulgghm  19846  srglmhm  20218  srgrmhm  20219  ringlghm  20309  ringrghm  20310  gsumdixp  20316  isrhm  20478  rhmval  20500  issrngd  20856  lmodvsghm  20921  pwssplit2  21059  xrsdsval  21428  expmhm  21454  expghm  21486  mulgghm2  21487  mulgrhm  21488  pzriprnglem4  21495  cygznlem3  21588  asclghm  21903  psrmulfval  21963  evlslem4  22100  mpfrcl  22109  mamuval  22397  mamufv  22398  mvmulval  22549  mndifsplit  22642  mat2pmatmul  22737  decpmatmul  22778  fmval  23951  fmf  23953  flffval  23997  divcnOLD  24890  divcn  24892  rescncf  24923  htpyco1  25010  tcphcph  25271  rrxdsfival  25447  ehl2eudisval  25457  volun  25580  dyadval  25627  dvlip  26032  ftc1a  26078  ftc2ditglem  26086  tdeglem3  26098  q1pval  26194  reefgim  26494  relogoprlem  26633  eflogeq  26644  zetacvg  27058  lgsdir2  27374  lgsdchr  27399  2sq2  27477  2sqnn0  27482  negsdi  28082  brbtwn2  28920  ax5seglem4  28947  axeuclid  28978  axcontlem2  28980  axcontlem4  28982  axcontlem8  28986  clwwlknccat  30082  ex-fpar  30481  ipasslem11  30859  hhssnv  31283  mayete3i  31747  idunop  31997  idhmop  32001  0lnfn  32004  lnopmi  32019  lnophsi  32020  lnopcoi  32022  hmops  32039  hmopm  32040  nlelshi  32079  cnlnadjlem2  32087  kbass6  32140  strlem3a  32271  hstrlem3a  32279  elrgspnlem2  33247  mndpluscn  33925  xrge0iifhom  33936  rezh  33970  probdsb  34424  resconn  35251  iscvm  35264  satfdmlem  35373  satffunlem1lem1  35407  satffunlem2lem1  35409  fwddifnval  36164  bj-bary1  37313  poimirlem15  37642  mbfposadd  37674  ftc1anclem3  37702  rrnmval  37835  dvhopaddN  41116  nnadddir  42305  cnreeu  42500  prjcrvfval  42641  pellex  42846  rmxfval  42915  rmyfval  42916  qirropth  42919  rmxycomplete  42929  jm2.15nn0  43015  rmxdioph  43028  expdiophlem2  43034  mendvsca  43199  deg1mhm  43212  mnringmulrvald  44246  addrval  44485  subrval  44486  fmulcl  45596  fmuldfeqlem1  45597  line  48653  itsclc0xyqsolr  48690