Theorem oveqan12d 7449

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1536  (class class class)co 7430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433

This theorem is referenced by:  oveqan12rd  7450  offval  7705  offval3  8005  odi  8615  omopth2  8620  oeoa  8633  ecovdi  8863  ackbij1lem9  10264  distrpi  10935  addpipq  10974  mulpipq  10977  lterpq  11007  reclem3pr  11086  1idsr  11135  mulcnsr  11173  mulrid  11256  1re  11258  mul02  11436  addcom  11444  mulsub  11703  mulsub2  11704  muleqadd  11904  divmuldiv  11964  div2sub  12089  addltmul  12499  xnegdi  13286  xadddilem  13332  fzsubel  13596  fzoval  13696  seqid3  14083  mulexp  14138  sqdiv  14157  hashdom  14414  hashun  14417  ccatfval  14607  splcl  14786  crim  15150  readd  15161  remullem  15163  imadd  15169  cjadd  15176  cjreim  15195  sqrtmul  15294  sqabsadd  15317  sqabssub  15318  absmul  15329  abs2dif  15367  bhmafibid1  15500  binom  15862  binomfallfac  16073  sinadd  16196  cosadd  16197  dvds2ln  16322  sadcaddlem  16490  bezoutlem4  16575  bezout  16576  absmulgcd  16582  gcddiv  16584  bezoutr1  16602  lcmgcd  16640  lcmfass  16679  nn0gcdsq  16785  crth  16811  pythagtriplem1  16849  pcqmul  16886  4sqlem4a  16984  4sqlem4  16985  prdsplusgval  17519  prdsmulrval  17521  prdsdsval  17524  prdsvscaval  17525  idmgmhm  18726  resmgmhm  18736  idmhm  18820  0mhm  18844  resmhm  18845  prdspjmhm  18854  pwsdiagmhm  18856  gsumws2  18867  frmdup1  18889  eqgval  19207  idghm  19261  resghm  19262  mulgmhm  19859  mulgghm  19860  srglmhm  20238  srgrmhm  20239  ringlghm  20325  ringrghm  20326  gsumdixp  20332  isrhm  20494  rhmval  20516  issrngd  20872  lmodvsghm  20937  pwssplit2  21076  xrsdsval  21445  expmhm  21471  expghm  21503  mulgghm2  21504  mulgrhm  21505  pzriprnglem4  21512  cygznlem3  21605  asclghm  21920  psrmulfval  21980  evlslem4  22117  mpfrcl  22126  mamuval  22412  mamufv  22413  mvmulval  22564  mndifsplit  22657  mat2pmatmul  22752  decpmatmul  22793  fmval  23966  fmf  23968  flffval  24012  divcnOLD  24903  divcn  24905  rescncf  24936  htpyco1  25023  tcphcph  25284  rrxdsfival  25460  ehl2eudisval  25470  volun  25593  dyadval  25640  dvlip  26046  ftc1a  26092  ftc2ditglem  26100  tdeglem3  26112  q1pval  26208  reefgim  26508  relogoprlem  26647  eflogeq  26658  zetacvg  27072  lgsdir2  27388  lgsdchr  27413  2sq2  27491  2sqnn0  27496  negsdi  28096  brbtwn2  28934  ax5seglem4  28961  axeuclid  28992  axcontlem2  28994  axcontlem4  28996  axcontlem8  29000  clwwlknccat  30091  ex-fpar  30490  ipasslem11  30868  hhssnv  31292  mayete3i  31756  idunop  32006  idhmop  32010  0lnfn  32013  lnopmi  32028  lnophsi  32029  lnopcoi  32031  hmops  32048  hmopm  32049  nlelshi  32088  cnlnadjlem2  32096  kbass6  32149  strlem3a  32280  hstrlem3a  32288  elrgspnlem2  33232  mndpluscn  33886  xrge0iifhom  33897  rezh  33931  probdsb  34403  resconn  35230  iscvm  35243  satfdmlem  35352  satffunlem1lem1  35386  satffunlem2lem1  35388  fwddifnval  36144  bj-bary1  37294  poimirlem15  37621  mbfposadd  37653  ftc1anclem3  37681  rrnmval  37814  dvhopaddN  41096  nnadddir  42283  cnreeu  42476  prjcrvfval  42617  pellex  42822  rmxfval  42891  rmyfval  42892  qirropth  42895  rmxycomplete  42905  jm2.15nn0  42991  rmxdioph  43004  expdiophlem2  43010  mendvsca  43175  deg1mhm  43188  mnringmulrvald  44222  addrval  44461  subrval  44462  fmulcl  45536  fmuldfeqlem1  45537  line  48581  itsclc0xyqsolr  48618