Theorem oveqan12d 7409

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559  (class class class)co 7390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6471  df-fv 6523  df-ov 7393

This theorem is referenced by:  oveqan12rd  7410  offval  7663  offval3  7957  odi  8541  omopth2  8546  oeoa  8560  ecovdi  8800  ackbij1lem9  10178  distrpi  10851  addpipq  10890  mulpipq  10893  lterpq  10923  reclem3pr  11002  1idsr  11051  mulcnsr  11089  mulrid  11174  1re  11176  mul02  11356  addcom  11364  mulsub  11625  mulsub2  11626  muleqadd  11826  divmuldiv  11886  div2sub  12011  nnadddir  12264  addltmul  12452  xnegdi  13246  xadddilem  13292  fzsubel  13560  fzoval  13660  seqid3  14054  mulexp  14109  sqdiv  14129  hashdom  14387  hashun  14390  ccatfval  14581  splcl  14760  crim  15123  readd  15134  remullem  15136  imadd  15142  cjadd  15149  cjreim  15168  sqrtmul  15267  sqabsadd  15290  sqabssub  15291  absmul  15302  abs2dif  15341  bhmafibid1  15476  binom  15841  binomfallfac  16052  sinadd  16177  cosadd  16178  dvds2ln  16304  sadcaddlem  16472  bezoutlem4  16557  bezout  16558  absmulgcd  16564  gcddiv  16566  bezoutr1  16584  lcmgcd  16622  lcmfass  16661  nn0gcdsq  16768  crth  16794  pythagtriplem1  16833  pcqmul  16870  4sqlem4a  16968  4sqlem4  16969  prdsplusgval  17483  prdsmulrval  17485  prdsdsval  17488  prdsvscaval  17489  idmgmhm  18716  resmgmhm  18726  idmhm  18810  0mhm  18834  resmhm  18835  prdspjmhm  18844  pwsdiagmhm  18846  gsumws2  18857  frmdup1  18879  eqgval  19199  idghm  19252  resghm  19253  mulgmhm  19848  mulgghm  19849  srglmhm  20248  srgrmhm  20249  ringlghm  20339  ringrghm  20340  gsumdixp  20344  isrhm  20504  rhmval  20526  issrngd  20882  lmodvsghm  20968  pwssplit2  21105  xrsdsval  21441  expmhm  21466  expghm  21505  mulgghm2  21506  mulgrhm  21507  pzriprnglem4  21514  cygznlem3  21599  asclghm  21912  psrmulfval  21973  evlslem4  22107  mpfrcl  22116  mamuval  22431  mamufv  22432  mvmulval  22581  mndifsplit  22674  mat2pmatmul  22769  decpmatmul  22810  fmval  23981  fmf  23983  flffval  24027  divcn  24908  rescncf  24937  htpyco1  25018  tcphcph  25277  rrxdsfival  25453  ehl2eudisval  25463  volun  25585  dyadval  25632  dvlip  26033  ftc1a  26077  ftc2ditglem  26085  tdeglem3  26097  q1pval  26193  reefgim  26488  relogoprlem  26631  eflogeq  26642  zetacvg  27054  lgsdir2  27369  lgsdchr  27394  2sq2  27472  2sqnn0  27477  negsdi  28118  brbtwn2  29050  ax5seglem4  29077  axeuclid  29108  axcontlem2  29110  axcontlem4  29112  axcontlem8  29116  clwwlknccat  30209  ex-fpar  30608  ipasslem11  30987  hhssnv  31411  mayete3i  31875  idunop  32125  idhmop  32129  0lnfn  32132  lnopmi  32147  lnophsi  32148  lnopcoi  32150  hmops  32167  hmopm  32168  nlelshi  32207  cnlnadjlem2  32215  kbass6  32268  strlem3a  32399  hstrlem3a  32407  elrgspnlem2  33383  mndpluscn  34182  xrge0iifhom  34193  rezh  34225  probdsb  34678  resconn  35549  iscvm  35562  satfdmlem  35671  satffunlem1lem1  35705  satffunlem2lem1  35707  fwddifnval  36466  bj-bary1  37757  poimirlem15  38087  mbfposadd  38119  ftc1anclem3  38147  rrnmval  38280  dvhopaddN  41691  cnreeu  43065  prjcrvfval  43166  pellex  43365  rmxfval  43434  rmyfval  43435  qirropth  43438  rmxycomplete  43447  jm2.15nn0  43533  rmxdioph  43546  expdiophlem2  43552  mendvsca  43717  deg1mhm  43730  mnringmulrvald  44756  addrval  44994  subrval  44995  fmulcl  46110  fmuldfeqlem1  46111  line  49307  itsclc0xyqsolr  49344