Theorem oveqan12d 7368

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

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

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352

This theorem is referenced by:  oveqan12rd  7369  offval  7622  offval3  7917  odi  8497  omopth2  8502  oeoa  8515  ecovdi  8752  ackbij1lem9  10121  distrpi  10792  addpipq  10831  mulpipq  10834  lterpq  10864  reclem3pr  10943  1idsr  10992  mulcnsr  11030  mulrid  11113  1re  11115  mul02  11294  addcom  11302  mulsub  11563  mulsub2  11564  muleqadd  11764  divmuldiv  11824  div2sub  11949  addltmul  12360  xnegdi  13150  xadddilem  13196  fzsubel  13463  fzoval  13563  seqid3  13953  mulexp  14008  sqdiv  14028  hashdom  14286  hashun  14289  ccatfval  14480  splcl  14658  crim  15022  readd  15033  remullem  15035  imadd  15041  cjadd  15048  cjreim  15067  sqrtmul  15166  sqabsadd  15189  sqabssub  15190  absmul  15201  abs2dif  15240  bhmafibid1  15375  binom  15737  binomfallfac  15948  sinadd  16073  cosadd  16074  dvds2ln  16200  sadcaddlem  16368  bezoutlem4  16453  bezout  16454  absmulgcd  16460  gcddiv  16462  bezoutr1  16480  lcmgcd  16518  lcmfass  16557  nn0gcdsq  16663  crth  16689  pythagtriplem1  16728  pcqmul  16765  4sqlem4a  16863  4sqlem4  16864  prdsplusgval  17377  prdsmulrval  17379  prdsdsval  17382  prdsvscaval  17383  idmgmhm  18575  resmgmhm  18585  idmhm  18669  0mhm  18693  resmhm  18694  prdspjmhm  18703  pwsdiagmhm  18705  gsumws2  18716  frmdup1  18738  eqgval  19056  idghm  19110  resghm  19111  mulgmhm  19706  mulgghm  19707  srglmhm  20106  srgrmhm  20107  ringlghm  20197  ringrghm  20198  gsumdixp  20204  isrhm  20363  rhmval  20385  issrngd  20740  lmodvsghm  20826  pwssplit2  20964  xrsdsval  21317  expmhm  21343  expghm  21382  mulgghm2  21383  mulgrhm  21384  pzriprnglem4  21391  cygznlem3  21476  asclghm  21790  psrmulfval  21850  evlslem4  21981  mpfrcl  21990  mamuval  22278  mamufv  22279  mvmulval  22428  mndifsplit  22521  mat2pmatmul  22616  decpmatmul  22657  fmval  23828  fmf  23830  flffval  23874  divcnOLD  24755  divcn  24757  rescncf  24788  htpyco1  24875  tcphcph  25135  rrxdsfival  25311  ehl2eudisval  25321  volun  25444  dyadval  25491  dvlip  25896  ftc1a  25942  ftc2ditglem  25950  tdeglem3  25962  q1pval  26058  reefgim  26358  relogoprlem  26498  eflogeq  26509  zetacvg  26923  lgsdir2  27239  lgsdchr  27264  2sq2  27342  2sqnn0  27347  negsdi  27963  brbtwn2  28854  ax5seglem4  28881  axeuclid  28912  axcontlem2  28914  axcontlem4  28916  axcontlem8  28920  clwwlknccat  30011  ex-fpar  30410  ipasslem11  30788  hhssnv  31212  mayete3i  31676  idunop  31926  idhmop  31930  0lnfn  31933  lnopmi  31948  lnophsi  31949  lnopcoi  31951  hmops  31968  hmopm  31969  nlelshi  32008  cnlnadjlem2  32016  kbass6  32069  strlem3a  32200  hstrlem3a  32208  elrgspnlem2  33192  mndpluscn  33909  xrge0iifhom  33920  rezh  33952  probdsb  34406  resconn  35239  iscvm  35252  satfdmlem  35361  satffunlem1lem1  35395  satffunlem2lem1  35397  fwddifnval  36157  bj-bary1  37306  poimirlem15  37635  mbfposadd  37667  ftc1anclem3  37695  rrnmval  37828  dvhopaddN  41113  nnadddir  42263  cnreeu  42483  prjcrvfval  42624  pellex  42828  rmxfval  42897  rmyfval  42898  qirropth  42901  rmxycomplete  42910  jm2.15nn0  42996  rmxdioph  43009  expdiophlem2  43015  mendvsca  43180  deg1mhm  43193  mnringmulrvald  44220  addrval  44459  subrval  44460  fmulcl  45582  fmuldfeqlem1  45583  line  48737  itsclc0xyqsolr  48774