Theorem oveqan12d 6546

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

Syntax hints:   → wi 4   ∧ wa 382   = wceq 1474  (class class class)co 6527

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rex 2901  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-iota 5754  df-fv 5798  df-ov 6530

This theorem is referenced by:  oveqan12rd  6547  offval  6779  offval3  7030  odi  7523  omopth2  7528  oeoa  7541  ecovdi  7720  ackbij1lem9  8910  alephadd  9255  distrpi  9576  addpipq  9615  mulpipq  9618  lterpq  9648  reclem3pr  9727  1idsr  9775  mulcnsr  9813  mulid1  9893  1re  9895  mul02  10065  addcom  10073  mulsub  10323  mulsub2  10324  muleqadd  10520  divmuldiv  10574  div2sub  10699  addltmul  11115  xnegdi  11907  xadddilem  11953  fzsubel  12203  fzoval  12295  seqid3  12662  mulexp  12716  sqdiv  12745  hashdom  12981  hashun  12984  ccatfval  13157  splcl  13300  crim  13649  readd  13660  remullem  13662  imadd  13668  cjadd  13675  cjreim  13694  sqrtmul  13794  sqabsadd  13816  sqabssub  13817  absmul  13828  abs2dif  13866  binom  14347  binomfallfac  14557  sinadd  14679  cosadd  14680  dvds2ln  14798  sadcaddlem  14963  bezoutlem4  15043  bezout  15044  absmulgcd  15050  gcddiv  15052  bezoutr1  15066  lcmgcd  15104  lcmfass  15143  nn0gcdsq  15244  crth  15267  pythagtriplem1  15305  pcqmul  15342  4sqlem4a  15439  4sqlem4  15440  prdsplusgval  15902  prdsmulrval  15904  prdsdsval  15907  prdsvscaval  15908  xpsfval  15996  xpsval  16001  idmhm  17113  0mhm  17127  resmhm  17128  prdspjmhm  17136  pwsdiagmhm  17138  gsumws2  17148  frmdup1  17170  eqgval  17412  idghm  17444  resghm  17445  mulgmhm  18002  mulgghm  18003  srglmhm  18304  srgrmhm  18305  ringlghm  18373  ringrghm  18374  gsumdixp  18378  isrhm  18490  issrngd  18630  lmodvsghm  18693  pwssplit2  18827  asclghm  19105  psrmulfval  19152  evlslem4  19275  mpfrcl  19285  xrsdsval  19555  expmhm  19580  expghm  19608  mulgghm2  19609  mulgrhm  19610  cygznlem3  19682  mamuval  19953  mamufv  19954  mvmulval  20110  mndifsplit  20203  mat2pmatmul  20297  decpmatmul  20338  fmval  21499  fmf  21501  flffval  21545  divcn  22410  rescncf  22439  htpyco1  22516  tchcph  22765  volun  23037  dyadval  23083  dvlip  23477  ftc1a  23521  ftc2ditglem  23529  tdeglem3  23540  q1pval  23634  reefgim  23925  relogoprlem  24058  eflogeq  24069  zetacvg  24458  lgsdir2  24772  lgsdchr  24797  brbtwn2  25503  ax5seglem4  25530  axeuclid  25561  axcontlem2  25563  axcontlem4  25565  axcontlem8  25569  numclwlk1lem2fo  26388  ipasslem11  26885  hhssnv  27311  mayete3i  27777  idunop  28027  idhmop  28031  0lnfn  28034  lnopmi  28049  lnophsi  28050  lnopcoi  28052  hmops  28069  hmopm  28070  nlelshi  28109  cnlnadjlem2  28117  kbass6  28170  strlem3a  28301  hstrlem3a  28309  bhmafibid1  28781  mndpluscn  29106  xrge0iifhom  29117  rezh  29149  probdsb  29617  rescon  30288  iscvm  30301  fwddifnval  31246  bj-bary1  32135  poimirlem15  32390  mbfposadd  32423  ftc1anclem3  32453  rrnmval  32593  dvhopaddN  35217  pellex  36213  rmxfval  36282  rmyfval  36283  qirropth  36287  rmxycomplete  36296  jm2.15nn0  36384  rmxdioph  36397  expdiophlem2  36403  mendvsca  36576  deg1mhm  36600  addrval  37487  subrval  37488  fmulcl  38445  fmuldfeqlem1  38446  av-numclwlk1lem2fo  41520  idmgmhm  41573  resmgmhm  41583  rhmval  41704  offval0  42088