Theorem oveqan12d 7431

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   = wceq 1569  (class class class)co 7412

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-v 3456  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 7415

This theorem is used by:  oveqan12rd  7432  offval  7685  offval3  7977  odi  8562  omopth2  8567  oeoa  8581  ecovdi  8821  ackbij1lem9  10217  distrpi  10889  addpipq  10928  mulpipq  10931  lterpq  10961  reclem3pr  11040  1idsr  11089  mulcnsr  11127  mulrid  11212  1re  11214  mul02  11394  addcom  11402  mulsub  11663  mulsub2  11664  muleqadd  11864  divmuldiv  11921  div2sub  12046  nnadddir  12298  addltmul  12486  xnegdi  13280  xadddilem  13326  fzsubel  13595  fzoval  13695  seqid3  14089  mulexp  14144  sqdiv  14164  hashdom  14422  hashun  14425  ccatfval  14617  splcl  14796  crim  15173  readd  15184  remullem  15186  imadd  15192  cjadd  15199  cjreim  15218  sqrtmul  15317  sqabsadd  15340  sqabssub  15341  absmul  15352  abs2dif  15391  bhmafibid1  15526  binom  15891  binomfallfac  16101  sinadd  16226  cosadd  16227  dvds2ln  16353  sadcaddlem  16521  bezoutlem4  16606  bezout  16607  absmulgcd  16613  gcddiv  16615  bezoutr1  16633  lcmgcd  16671  lcmfass  16710  nn0gcdsq  16817  crth  16843  pythagtriplem1  16882  pcqmul  16919  4sqlem4a  17017  4sqlem4  17018  prdsplusgval  17532  prdsmulrval  17534  prdsdsval  17537  prdsvscaval  17538  idmgmhm  18765  resmgmhm  18775  idmhm  18859  0mhm  18884  resmhm  18885  prdspjmhm  18894  pwsdiagmhm  18896  gsumws2  18907  frmdup1  18929  eqgval  19251  idghm  19307  resghm  19308  mulgmhm  19903  mulgghm  19904  srglmhm  20309  srgrmhm  20310  ringlghm  20402  ringrghm  20403  gsumdixp  20407  isrhm  20568  rhmval  20597  issrngd  20969  lmodvsghm  21055  pwssplit2  21192  xrsdsval  21572  expmhm  21597  expghm  21636  mulgghm2  21637  mulgrhm  21638  pzriprnglem4  21645  cygznlem3  21730  asclghm  22043  psrmulfval  22104  evlslem4  22238  mpfrcl  22247  mamuval  22561  mamufv  22562  mvmulval  22711  mndifsplit  22804  mat2pmatmul  22899  decpmatmul  22940  fmval  24111  fmf  24113  flffval  24157  divcn  25038  rescncf  25067  htpyco1  25148  tcphcph  25407  rrxdsfival  25583  ehl2eudisval  25593  volun  25715  dyadval  25762  dvlip  26163  ftc1a  26207  ftc2ditglem  26215  tdeglem3  26227  q1pval  26323  reefgim  26624  relogoprlem  26767  eflogeq  26778  zetacvg  27190  lgsdir2  27505  lgsdchr  27530  2sq2  27608  2sqnn0  27613  negsdi  28254  brbtwn2  29266  ax5seglem4  29293  axeuclid  29324  axcontlem2  29326  axcontlem4  29328  axcontlem8  29332  clwwlknccat  30425  ex-fpar  30824  ipasslem11  31203  hhssnv  31627  mayete3i  32091  idunop  32341  idhmop  32345  0lnfn  32348  lnopmi  32363  lnophsi  32364  lnopcoi  32366  hmops  32383  hmopm  32384  nlelshi  32423  cnlnadjlem2  32431  kbass6  32484  strlem3a  32615  hstrlem3a  32623  elrgspnlem2  33572  mndpluscn  34325  xrge0iifhom  34336  rezh  34368  probdsb  34821  resconn  35746  iscvm  35759  satfdmlem  35868  satffunlem1lem1  35902  satffunlem2lem1  35904  fwddifnval  36663  bj-bary1  37984  poimirlem15  38314  mbfposadd  38346  ftc1anclem3  38374  rrnmval  38507  dvhopaddN  41916  cnreeu  43292  prjcrvfval  43391  pellex  43590  rmxfval  43659  rmyfval  43660  qirropth  43663  rmxycomplete  43672  jm2.15nn0  43758  rmxdioph  43771  expdiophlem2  43777  mendvsca  43942  deg1mhm  43955  mnringmulrvald  44979  addrval  45202  subrval  45203  hashnna  45756  fmulcl  46325  fmuldfeqlem1  46326  line  49540  itsclc0xyqsolr  49577