Theorem oveqan12d 7435

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570  (class class class)co 7416

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7419

This theorem is used by:  oveqan12rd  7436  offval  7690  offval3  7982  odi  8569  omopth2  8574  oeoa  8588  ecovdi  8828  ackbij1lem9  10232  distrpi  10910  addpipq  10949  mulpipq  10952  lterpq  10982  reclem3pr  11061  1idsr  11110  mulcnsr  11148  mulrid  11233  1re  11235  mul02  11415  addcom  11423  mulsub  11684  mulsub2  11685  muleqadd  11885  divmuldiv  11942  div2sub  12067  nnadddir  12319  addltmul  12507  xnegdi  13302  xadddilem  13348  fzsubel  13617  fzoval  13717  seqid3  14112  mulexp  14167  sqdiv  14187  hashdom  14445  hashun  14448  ccatfval  14640  splcl  14823  crim  15204  readd  15215  remullem  15217  imadd  15223  cjadd  15230  cjreim  15249  sqrtmul  15348  sqabsadd  15371  sqabssub  15372  absmul  15383  abs2dif  15422  bhmafibid1  15557  binom  15921  binomfallfac  16131  sinadd  16256  cosadd  16257  dvds2ln  16383  sadcaddlem  16551  bezoutlem4  16636  bezout  16637  absmulgcd  16643  gcddiv  16645  bezoutr1  16663  lcmgcd  16701  lcmfass  16740  nn0gcdsq  16847  crth  16873  pythagtriplem1  16912  pcqmul  16949  4sqlem4a  17047  4sqlem4  17048  prdsplusgval  17562  prdsmulrval  17564  prdsdsval  17567  prdsvscaval  17568  idmgmhm  18805  resmgmhm  18815  idmhm  18904  0mhm  18929  resmhm  18930  prdspjmhm  18939  pwsdiagmhm  18941  gsumws2  18952  frmdup1  18974  eqgval  19303  idghm  19359  resghm  19360  mulgmhm  19955  mulgghm  19956  srglmhm  20361  srgrmhm  20362  ringlghm  20455  ringrghm  20456  gsumdixp  20460  isrhm  20621  rhmval  20650  issrngd  21022  lmodvsghm  21108  pwssplit2  21245  xrsdsval  21625  expmhm  21650  expghm  21689  mulgghm2  21690  mulgrhm  21691  pzriprnglem4  21698  cygznlem3  21783  asclghm  22098  psrmulfval  22159  evlslem4  22293  mpfrcl  22302  mamuval  22616  mamufv  22617  mvmulval  22766  mndifsplit  22859  mat2pmatmul  22957  decpmatmul  22998  fmval  24170  fmf  24172  flffval  24216  divcn  25097  rescncf  25126  htpyco1  25207  tcphcph  25466  rrxdsfival  25642  ehl2eudisval  25652  volun  25774  dyadval  25821  dvlip  26222  ftc1a  26266  ftc2ditglem  26274  tdeglem3  26286  q1pval  26382  reefgim  26683  relogoprlem  26826  eflogeq  26837  zetacvg  27249  lgsdir2  27564  lgsdchr  27589  2sq2  27667  2sqnn0  27672  negsdi  28313  brbtwn2  29348  ax5seglem4  29375  axeuclid  29406  axcontlem2  29408  axcontlem4  29410  axcontlem8  29414  clwwlknccat  30519  ex-fpar  30928  ipasslem11  31307  hhssnv  31731  mayete3i  32195  idunop  32445  idhmop  32449  0lnfn  32452  lnopmi  32467  lnophsi  32468  lnopcoi  32470  hmops  32487  hmopm  32488  nlelshi  32527  cnlnadjlem2  32535  kbass6  32588  strlem3a  32719  hstrlem3a  32727  elrgspnlem2  33670  mndpluscn  34423  xrge0iifhom  34434  rezh  34466  probdsb  34920  resconn  35812  iscvm  35825  satfdmlem  35934  satffunlem1lem1  35968  satffunlem2lem1  35970  fwddifnval  36730  bj-bary1  38051  poimirlem15  38371  mbfposadd  38403  ftc1anclem3  38431  rrnmval  38565  dvhopaddN  41974  cnreeu  43365  prjcrvfval  43464  pellex  43663  rmxfval  43732  rmyfval  43733  qirropth  43736  rmxycomplete  43745  jm2.15nn0  43831  rmxdioph  43844  expdiophlem2  43850  mendvsca  44015  deg1mhm  44028  mnringmulrvald  45052  addrval  45275  subrval  45276  hashnna  45829  fmulcl  46398  fmuldfeqlem1  46399  line  49649  itsclc0xyqsolr  49686