Theorem oveqan12d 7422

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538  df-ov 7406

This theorem is referenced by:  oveqan12rd  7423  offval  7678  offval3  7979  odi  8589  omopth2  8594  oeoa  8607  ecovdi  8837  ackbij1lem9  10239  distrpi  10910  addpipq  10949  mulpipq  10952  lterpq  10982  reclem3pr  11061  1idsr  11110  mulcnsr  11148  mulrid  11231  1re  11233  mul02  11411  addcom  11419  mulsub  11678  mulsub2  11679  muleqadd  11879  divmuldiv  11939  div2sub  12064  addltmul  12475  xnegdi  13262  xadddilem  13308  fzsubel  13575  fzoval  13675  seqid3  14062  mulexp  14117  sqdiv  14137  hashdom  14395  hashun  14398  ccatfval  14589  splcl  14768  crim  15132  readd  15143  remullem  15145  imadd  15151  cjadd  15158  cjreim  15177  sqrtmul  15276  sqabsadd  15299  sqabssub  15300  absmul  15311  abs2dif  15349  bhmafibid1  15482  binom  15844  binomfallfac  16055  sinadd  16180  cosadd  16181  dvds2ln  16306  sadcaddlem  16474  bezoutlem4  16559  bezout  16560  absmulgcd  16566  gcddiv  16568  bezoutr1  16586  lcmgcd  16624  lcmfass  16663  nn0gcdsq  16769  crth  16795  pythagtriplem1  16834  pcqmul  16871  4sqlem4a  16969  4sqlem4  16970  prdsplusgval  17485  prdsmulrval  17487  prdsdsval  17490  prdsvscaval  17491  idmgmhm  18677  resmgmhm  18687  idmhm  18771  0mhm  18795  resmhm  18796  prdspjmhm  18805  pwsdiagmhm  18807  gsumws2  18818  frmdup1  18840  eqgval  19158  idghm  19212  resghm  19213  mulgmhm  19806  mulgghm  19807  srglmhm  20179  srgrmhm  20180  ringlghm  20270  ringrghm  20271  gsumdixp  20277  isrhm  20436  rhmval  20458  issrngd  20813  lmodvsghm  20878  pwssplit2  21016  xrsdsval  21376  expmhm  21402  expghm  21434  mulgghm2  21435  mulgrhm  21436  pzriprnglem4  21443  cygznlem3  21528  asclghm  21841  psrmulfval  21901  evlslem4  22032  mpfrcl  22041  mamuval  22329  mamufv  22330  mvmulval  22479  mndifsplit  22572  mat2pmatmul  22667  decpmatmul  22708  fmval  23879  fmf  23881  flffval  23925  divcnOLD  24806  divcn  24808  rescncf  24839  htpyco1  24926  tcphcph  25187  rrxdsfival  25363  ehl2eudisval  25373  volun  25496  dyadval  25543  dvlip  25948  ftc1a  25994  ftc2ditglem  26002  tdeglem3  26014  q1pval  26110  reefgim  26410  relogoprlem  26550  eflogeq  26561  zetacvg  26975  lgsdir2  27291  lgsdchr  27316  2sq2  27394  2sqnn0  27399  negsdi  27999  brbtwn2  28830  ax5seglem4  28857  axeuclid  28888  axcontlem2  28890  axcontlem4  28892  axcontlem8  28896  clwwlknccat  29990  ex-fpar  30389  ipasslem11  30767  hhssnv  31191  mayete3i  31655  idunop  31905  idhmop  31909  0lnfn  31912  lnopmi  31927  lnophsi  31928  lnopcoi  31930  hmops  31947  hmopm  31948  nlelshi  31987  cnlnadjlem2  31995  kbass6  32048  strlem3a  32179  hstrlem3a  32187  elrgspnlem2  33184  mndpluscn  33903  xrge0iifhom  33914  rezh  33946  probdsb  34400  resconn  35214  iscvm  35227  satfdmlem  35336  satffunlem1lem1  35370  satffunlem2lem1  35372  fwddifnval  36127  bj-bary1  37276  poimirlem15  37605  mbfposadd  37637  ftc1anclem3  37665  rrnmval  37798  dvhopaddN  41079  nnadddir  42267  cnreeu  42460  prjcrvfval  42601  pellex  42805  rmxfval  42874  rmyfval  42875  qirropth  42878  rmxycomplete  42888  jm2.15nn0  42974  rmxdioph  42987  expdiophlem2  42993  mendvsca  43158  deg1mhm  43171  mnringmulrvald  44199  addrval  44438  subrval  44439  fmulcl  45558  fmuldfeqlem1  45559  line  48660  itsclc0xyqsolr  48697