Theorem oveqan12d 7375

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542  (class class class)co 7356

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-rab 3388  df-v 3429  df-dif 3888  df-un 3890  df-ss 3902  df-nul 4264  df-if 4457  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-br 5075  df-iota 6443  df-fv 6495  df-ov 7359

This theorem is referenced by:  oveqan12rd  7376  offval  7629  offval3  7924  odi  8503  omopth2  8508  oeoa  8522  ecovdi  8761  ackbij1lem9  10138  distrpi  10810  addpipq  10849  mulpipq  10852  lterpq  10882  reclem3pr  10961  1idsr  11010  mulcnsr  11048  mulrid  11131  1re  11133  mul02  11313  addcom  11321  mulsub  11582  mulsub2  11583  muleqadd  11783  divmuldiv  11844  div2sub  11969  nnadddir  12222  addltmul  12402  xnegdi  13189  xadddilem  13235  fzsubel  13503  fzoval  13603  seqid3  13997  mulexp  14052  sqdiv  14072  hashdom  14330  hashun  14333  ccatfval  14524  splcl  14703  crim  15066  readd  15077  remullem  15079  imadd  15085  cjadd  15092  cjreim  15111  sqrtmul  15210  sqabsadd  15233  sqabssub  15234  absmul  15245  abs2dif  15284  bhmafibid1  15419  binom  15784  binomfallfac  15995  sinadd  16120  cosadd  16121  dvds2ln  16247  sadcaddlem  16415  bezoutlem4  16500  bezout  16501  absmulgcd  16507  gcddiv  16509  bezoutr1  16527  lcmgcd  16565  lcmfass  16604  nn0gcdsq  16711  crth  16737  pythagtriplem1  16776  pcqmul  16813  4sqlem4a  16911  4sqlem4  16912  prdsplusgval  17425  prdsmulrval  17427  prdsdsval  17430  prdsvscaval  17431  idmgmhm  18658  resmgmhm  18668  idmhm  18752  0mhm  18776  resmhm  18777  prdspjmhm  18786  pwsdiagmhm  18788  gsumws2  18799  frmdup1  18821  eqgval  19141  idghm  19195  resghm  19196  mulgmhm  19791  mulgghm  19792  srglmhm  20191  srgrmhm  20192  ringlghm  20282  ringrghm  20283  gsumdixp  20287  isrhm  20447  rhmval  20466  issrngd  20821  lmodvsghm  20907  pwssplit2  21044  xrsdsval  21380  expmhm  21405  expghm  21444  mulgghm2  21445  mulgrhm  21446  pzriprnglem4  21453  cygznlem3  21538  asclghm  21851  psrmulfval  21911  evlslem4  22043  mpfrcl  22052  mamuval  22346  mamufv  22347  mvmulval  22496  mndifsplit  22589  mat2pmatmul  22684  decpmatmul  22725  fmval  23896  fmf  23898  flffval  23942  divcn  24823  rescncf  24852  htpyco1  24933  tcphcph  25192  rrxdsfival  25368  ehl2eudisval  25378  volun  25500  dyadval  25547  dvlip  25948  ftc1a  25992  ftc2ditglem  26000  tdeglem3  26012  q1pval  26108  reefgim  26403  relogoprlem  26543  eflogeq  26554  zetacvg  26966  lgsdir2  27281  lgsdchr  27306  2sq2  27384  2sqnn0  27389  negsdi  28030  brbtwn2  28962  ax5seglem4  28989  axeuclid  29020  axcontlem2  29022  axcontlem4  29024  axcontlem8  29028  clwwlknccat  30121  ex-fpar  30520  ipasslem11  30899  hhssnv  31323  mayete3i  31787  idunop  32037  idhmop  32041  0lnfn  32044  lnopmi  32059  lnophsi  32060  lnopcoi  32062  hmops  32079  hmopm  32080  nlelshi  32119  cnlnadjlem2  32127  kbass6  32180  strlem3a  32311  hstrlem3a  32319  elrgspnlem2  33292  mndpluscn  34058  xrge0iifhom  34069  rezh  34101  probdsb  34554  resconn  35416  iscvm  35429  satfdmlem  35538  satffunlem1lem1  35572  satffunlem2lem1  35574  fwddifnval  36333  bj-bary1  37614  poimirlem15  37944  mbfposadd  37976  ftc1anclem3  38004  rrnmval  38137  dvhopaddN  41548  cnreeu  42923  prjcrvfval  43052  pellex  43251  rmxfval  43320  rmyfval  43321  qirropth  43324  rmxycomplete  43333  jm2.15nn0  43419  rmxdioph  43432  expdiophlem2  43438  mendvsca  43603  deg1mhm  43616  mnringmulrvald  44642  addrval  44880  subrval  44881  fmulcl  45999  fmuldfeqlem1  46000  line  49196  itsclc0xyqsolr  49233