Theorem oveqan12d 7400

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1550  (class class class)co 7381

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-rab 3405  df-v 3446  df-dif 3898  df-un 3900  df-ss 3912  df-nul 4277  df-if 4471  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-br 5091  df-iota 6462  df-fv 6514  df-ov 7384

This theorem is referenced by:  oveqan12rd  7401  offval  7654  offval3  7948  odi  8532  omopth2  8537  oeoa  8551  ecovdi  8791  ackbij1lem9  10169  distrpi  10842  addpipq  10881  mulpipq  10884  lterpq  10914  reclem3pr  10993  1idsr  11042  mulcnsr  11080  mulrid  11165  1re  11167  mul02  11347  addcom  11355  mulsub  11616  mulsub2  11617  muleqadd  11817  divmuldiv  11877  div2sub  12002  nnadddir  12255  addltmul  12443  xnegdi  13237  xadddilem  13283  fzsubel  13551  fzoval  13651  seqid3  14045  mulexp  14100  sqdiv  14120  hashdom  14378  hashun  14381  ccatfval  14572  splcl  14751  crim  15114  readd  15125  remullem  15127  imadd  15133  cjadd  15140  cjreim  15159  sqrtmul  15258  sqabsadd  15281  sqabssub  15282  absmul  15293  abs2dif  15332  bhmafibid1  15467  binom  15832  binomfallfac  16043  sinadd  16168  cosadd  16169  dvds2ln  16295  sadcaddlem  16463  bezoutlem4  16548  bezout  16549  absmulgcd  16555  gcddiv  16557  bezoutr1  16575  lcmgcd  16613  lcmfass  16652  nn0gcdsq  16759  crth  16785  pythagtriplem1  16824  pcqmul  16861  4sqlem4a  16959  4sqlem4  16960  prdsplusgval  17474  prdsmulrval  17476  prdsdsval  17479  prdsvscaval  17480  idmgmhm  18707  resmgmhm  18717  idmhm  18801  0mhm  18825  resmhm  18826  prdspjmhm  18835  pwsdiagmhm  18837  gsumws2  18848  frmdup1  18870  eqgval  19190  idghm  19243  resghm  19244  mulgmhm  19839  mulgghm  19840  srglmhm  20239  srgrmhm  20240  ringlghm  20330  ringrghm  20331  gsumdixp  20335  isrhm  20495  rhmval  20517  issrngd  20873  lmodvsghm  20959  pwssplit2  21096  xrsdsval  21432  expmhm  21457  expghm  21496  mulgghm2  21497  mulgrhm  21498  pzriprnglem4  21505  cygznlem3  21590  asclghm  21903  psrmulfval  21964  evlslem4  22098  mpfrcl  22107  mamuval  22422  mamufv  22423  mvmulval  22572  mndifsplit  22665  mat2pmatmul  22760  decpmatmul  22801  fmval  23972  fmf  23974  flffval  24018  divcn  24899  rescncf  24928  htpyco1  25009  tcphcph  25268  rrxdsfival  25444  ehl2eudisval  25454  volun  25576  dyadval  25623  dvlip  26024  ftc1a  26068  ftc2ditglem  26076  tdeglem3  26088  q1pval  26184  reefgim  26479  relogoprlem  26622  eflogeq  26633  zetacvg  27045  lgsdir2  27360  lgsdchr  27385  2sq2  27463  2sqnn0  27468  negsdi  28109  brbtwn2  29041  ax5seglem4  29068  axeuclid  29099  axcontlem2  29101  axcontlem4  29103  axcontlem8  29107  clwwlknccat  30200  ex-fpar  30599  ipasslem11  30978  hhssnv  31402  mayete3i  31866  idunop  32116  idhmop  32120  0lnfn  32123  lnopmi  32138  lnophsi  32139  lnopcoi  32141  hmops  32158  hmopm  32159  nlelshi  32198  cnlnadjlem2  32206  kbass6  32259  strlem3a  32390  hstrlem3a  32398  elrgspnlem2  33373  mndpluscn  34167  xrge0iifhom  34178  rezh  34210  probdsb  34663  resconn  35534  iscvm  35547  satfdmlem  35656  satffunlem1lem1  35690  satffunlem2lem1  35692  fwddifnval  36451  bj-bary1  37742  poimirlem15  38072  mbfposadd  38104  ftc1anclem3  38132  rrnmval  38265  dvhopaddN  41676  cnreeu  43050  prjcrvfval  43151  pellex  43350  rmxfval  43419  rmyfval  43420  qirropth  43423  rmxycomplete  43432  jm2.15nn0  43518  rmxdioph  43531  expdiophlem2  43537  mendvsca  43702  deg1mhm  43715  mnringmulrvald  44741  addrval  44979  subrval  44980  fmulcl  46095  fmuldfeqlem1  46096  line  49292  itsclc0xyqsolr  49329