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 596	1 ⊢ ((𝜑 ∧ 𝜓) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  (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 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393

This theorem is referenced by:  oveqan12rd  7410  offval  7665  offval3  7964  odi  8546  omopth2  8551  oeoa  8564  ecovdi  8801  ackbij1lem9  10187  distrpi  10858  addpipq  10897  mulpipq  10900  lterpq  10930  reclem3pr  11009  1idsr  11058  mulcnsr  11096  mulrid  11179  1re  11181  mul02  11359  addcom  11367  mulsub  11628  mulsub2  11629  muleqadd  11829  divmuldiv  11889  div2sub  12014  addltmul  12425  xnegdi  13215  xadddilem  13261  fzsubel  13528  fzoval  13628  seqid3  14018  mulexp  14073  sqdiv  14093  hashdom  14351  hashun  14354  ccatfval  14545  splcl  14724  crim  15088  readd  15099  remullem  15101  imadd  15107  cjadd  15114  cjreim  15133  sqrtmul  15232  sqabsadd  15255  sqabssub  15256  absmul  15267  abs2dif  15306  bhmafibid1  15441  binom  15803  binomfallfac  16014  sinadd  16139  cosadd  16140  dvds2ln  16266  sadcaddlem  16434  bezoutlem4  16519  bezout  16520  absmulgcd  16526  gcddiv  16528  bezoutr1  16546  lcmgcd  16584  lcmfass  16623  nn0gcdsq  16729  crth  16755  pythagtriplem1  16794  pcqmul  16831  4sqlem4a  16929  4sqlem4  16930  prdsplusgval  17443  prdsmulrval  17445  prdsdsval  17448  prdsvscaval  17449  idmgmhm  18635  resmgmhm  18645  idmhm  18729  0mhm  18753  resmhm  18754  prdspjmhm  18763  pwsdiagmhm  18765  gsumws2  18776  frmdup1  18798  eqgval  19116  idghm  19170  resghm  19171  mulgmhm  19764  mulgghm  19765  srglmhm  20137  srgrmhm  20138  ringlghm  20228  ringrghm  20229  gsumdixp  20235  isrhm  20394  rhmval  20416  issrngd  20771  lmodvsghm  20836  pwssplit2  20974  xrsdsval  21334  expmhm  21360  expghm  21392  mulgghm2  21393  mulgrhm  21394  pzriprnglem4  21401  cygznlem3  21486  asclghm  21799  psrmulfval  21859  evlslem4  21990  mpfrcl  21999  mamuval  22287  mamufv  22288  mvmulval  22437  mndifsplit  22530  mat2pmatmul  22625  decpmatmul  22666  fmval  23837  fmf  23839  flffval  23883  divcnOLD  24764  divcn  24766  rescncf  24797  htpyco1  24884  tcphcph  25144  rrxdsfival  25320  ehl2eudisval  25330  volun  25453  dyadval  25500  dvlip  25905  ftc1a  25951  ftc2ditglem  25959  tdeglem3  25971  q1pval  26067  reefgim  26367  relogoprlem  26507  eflogeq  26518  zetacvg  26932  lgsdir2  27248  lgsdchr  27273  2sq2  27351  2sqnn0  27356  negsdi  27963  brbtwn2  28839  ax5seglem4  28866  axeuclid  28897  axcontlem2  28899  axcontlem4  28901  axcontlem8  28905  clwwlknccat  29999  ex-fpar  30398  ipasslem11  30776  hhssnv  31200  mayete3i  31664  idunop  31914  idhmop  31918  0lnfn  31921  lnopmi  31936  lnophsi  31937  lnopcoi  31939  hmops  31956  hmopm  31957  nlelshi  31996  cnlnadjlem2  32004  kbass6  32057  strlem3a  32188  hstrlem3a  32196  elrgspnlem2  33201  mndpluscn  33923  xrge0iifhom  33934  rezh  33966  probdsb  34420  resconn  35240  iscvm  35253  satfdmlem  35362  satffunlem1lem1  35396  satffunlem2lem1  35398  fwddifnval  36158  bj-bary1  37307  poimirlem15  37636  mbfposadd  37668  ftc1anclem3  37696  rrnmval  37829  dvhopaddN  41115  nnadddir  42265  cnreeu  42485  prjcrvfval  42626  pellex  42830  rmxfval  42899  rmyfval  42900  qirropth  42903  rmxycomplete  42913  jm2.15nn0  42999  rmxdioph  43012  expdiophlem2  43018  mendvsca  43183  deg1mhm  43196  mnringmulrvald  44223  addrval  44462  subrval  44463  fmulcl  45586  fmuldfeqlem1  45587  line  48725  itsclc0xyqsolr  48762