Theorem oveqan12d 7429

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1568  (class class class)co 7410

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3415  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-iota 6492  df-fv 6544  df-ov 7413

This theorem is referenced by:  oveqan12rd  7430  offval  7683  offval3  7978  odi  8563  omopth2  8568  oeoa  8582  ecovdi  8822  ackbij1lem9  10209  distrpi  10882  addpipq  10921  mulpipq  10924  lterpq  10954  reclem3pr  11033  1idsr  11082  mulcnsr  11120  mulrid  11205  1re  11207  mul02  11387  addcom  11395  mulsub  11656  mulsub2  11657  muleqadd  11857  divmuldiv  11914  div2sub  12039  nnadddir  12291  addltmul  12479  xnegdi  13273  xadddilem  13319  fzsubel  13587  fzoval  13687  seqid3  14081  mulexp  14136  sqdiv  14156  hashdom  14414  hashun  14417  ccatfval  14609  splcl  14788  crim  15165  readd  15176  remullem  15178  imadd  15184  cjadd  15191  cjreim  15210  sqrtmul  15309  sqabsadd  15332  sqabssub  15333  absmul  15344  abs2dif  15383  bhmafibid1  15518  binom  15883  binomfallfac  16094  sinadd  16219  cosadd  16220  dvds2ln  16346  sadcaddlem  16514  bezoutlem4  16599  bezout  16600  absmulgcd  16606  gcddiv  16608  bezoutr1  16626  lcmgcd  16664  lcmfass  16703  nn0gcdsq  16810  crth  16836  pythagtriplem1  16875  pcqmul  16912  4sqlem4a  17010  4sqlem4  17011  prdsplusgval  17525  prdsmulrval  17527  prdsdsval  17530  prdsvscaval  17531  idmgmhm  18758  resmgmhm  18768  idmhm  18852  0mhm  18877  resmhm  18878  prdspjmhm  18887  pwsdiagmhm  18889  gsumws2  18900  frmdup1  18922  eqgval  19244  idghm  19300  resghm  19301  mulgmhm  19896  mulgghm  19897  srglmhm  20302  srgrmhm  20303  ringlghm  20394  ringrghm  20395  gsumdixp  20399  isrhm  20559  rhmval  20581  issrngd  20937  lmodvsghm  21023  pwssplit2  21160  xrsdsval  21540  expmhm  21565  expghm  21604  mulgghm2  21605  mulgrhm  21606  pzriprnglem4  21613  cygznlem3  21698  asclghm  22011  psrmulfval  22072  evlslem4  22206  mpfrcl  22215  mamuval  22529  mamufv  22530  mvmulval  22679  mndifsplit  22772  mat2pmatmul  22867  decpmatmul  22908  fmval  24079  fmf  24081  flffval  24125  divcn  25006  rescncf  25035  htpyco1  25116  tcphcph  25375  rrxdsfival  25551  ehl2eudisval  25561  volun  25683  dyadval  25730  dvlip  26131  ftc1a  26175  ftc2ditglem  26183  tdeglem3  26195  q1pval  26291  reefgim  26589  relogoprlem  26732  eflogeq  26743  zetacvg  27155  lgsdir2  27470  lgsdchr  27495  2sq2  27573  2sqnn0  27578  negsdi  28219  brbtwn2  29221  ax5seglem4  29248  axeuclid  29279  axcontlem2  29281  axcontlem4  29283  axcontlem8  29287  clwwlknccat  30380  ex-fpar  30779  ipasslem11  31158  hhssnv  31582  mayete3i  32046  idunop  32296  idhmop  32300  0lnfn  32303  lnopmi  32318  lnophsi  32319  lnopcoi  32321  hmops  32338  hmopm  32339  nlelshi  32378  cnlnadjlem2  32386  kbass6  32439  strlem3a  32570  hstrlem3a  32578  elrgspnlem2  33529  mndpluscn  34282  xrge0iifhom  34293  rezh  34325  probdsb  34778  resconn  35692  iscvm  35705  satfdmlem  35814  satffunlem1lem1  35848  satffunlem2lem1  35850  fwddifnval  36609  bj-bary1  37900  poimirlem15  38230  mbfposadd  38262  ftc1anclem3  38290  rrnmval  38423  dvhopaddN  41834  cnreeu  43210  prjcrvfval  43311  pellex  43510  rmxfval  43579  rmyfval  43580  qirropth  43583  rmxycomplete  43592  jm2.15nn0  43678  rmxdioph  43691  expdiophlem2  43697  mendvsca  43862  deg1mhm  43875  mnringmulrvald  44899  addrval  45122  subrval  45123  hashnna  45676  fmulcl  46245  fmuldfeqlem1  46246  line  49457  itsclc0xyqsolr  49494