Theorem oveqan12d 6709

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

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1523  (class class class)co 6690

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693

This theorem is referenced by:  oveqan12rd  6710  offval  6946  offval3  7204  odi  7704  omopth2  7709  oeoa  7722  ecovdi  7898  ackbij1lem9  9088  alephadd  9437  distrpi  9758  addpipq  9797  mulpipq  9800  lterpq  9830  reclem3pr  9909  1idsr  9957  mulcnsr  9995  mulid1  10075  1re  10077  mul02  10252  addcom  10260  mulsub  10511  mulsub2  10512  muleqadd  10709  divmuldiv  10763  div2sub  10888  addltmul  11306  xnegdi  12116  xadddilem  12162  fzsubel  12415  fzoval  12510  seqid3  12885  mulexp  12939  sqdiv  12968  hashdom  13206  hashun  13209  ccatfval  13391  splcl  13549  crim  13899  readd  13910  remullem  13912  imadd  13918  cjadd  13925  cjreim  13944  sqrtmul  14044  sqabsadd  14066  sqabssub  14067  absmul  14078  abs2dif  14116  binom  14606  binomfallfac  14816  sinadd  14938  cosadd  14939  dvds2ln  15061  sadcaddlem  15226  bezoutlem4  15306  bezout  15307  absmulgcd  15313  gcddiv  15315  bezoutr1  15329  lcmgcd  15367  lcmfass  15406  nn0gcdsq  15507  crth  15530  pythagtriplem1  15568  pcqmul  15605  4sqlem4a  15702  4sqlem4  15703  prdsplusgval  16180  prdsmulrval  16182  prdsdsval  16185  prdsvscaval  16186  xpsfval  16274  xpsval  16279  idmhm  17391  0mhm  17405  resmhm  17406  prdspjmhm  17414  pwsdiagmhm  17416  gsumws2  17426  frmdup1  17448  eqgval  17690  idghm  17722  resghm  17723  mulgmhm  18279  mulgghm  18280  srglmhm  18581  srgrmhm  18582  ringlghm  18650  ringrghm  18651  gsumdixp  18655  isrhm  18769  issrngd  18909  lmodvsghm  18972  pwssplit2  19108  asclghm  19386  psrmulfval  19433  evlslem4  19556  mpfrcl  19566  xrsdsval  19838  expmhm  19863  expghm  19892  mulgghm2  19893  mulgrhm  19894  cygznlem3  19966  mamuval  20240  mamufv  20241  mvmulval  20397  mndifsplit  20490  mat2pmatmul  20584  decpmatmul  20625  fmval  21794  fmf  21796  flffval  21840  divcn  22718  rescncf  22747  htpyco1  22824  tchcph  23082  volun  23359  dyadval  23406  dvlip  23801  ftc1a  23845  ftc2ditglem  23853  tdeglem3  23864  q1pval  23958  reefgim  24249  relogoprlem  24382  eflogeq  24393  zetacvg  24786  lgsdir2  25100  lgsdchr  25125  brbtwn2  25830  ax5seglem4  25857  axeuclid  25888  axcontlem2  25890  axcontlem4  25892  axcontlem8  25896  clwwlknccat  27333  ipasslem11  27823  hhssnv  28249  mayete3i  28715  idunop  28965  idhmop  28969  0lnfn  28972  lnopmi  28987  lnophsi  28988  lnopcoi  28990  hmops  29007  hmopm  29008  nlelshi  29047  cnlnadjlem2  29055  kbass6  29108  strlem3a  29239  hstrlem3a  29247  bhmafibid1  29772  mndpluscn  30100  xrge0iifhom  30111  rezh  30143  probdsb  30612  resconn  31354  iscvm  31367  fwddifnval  32395  bj-bary1  33292  poimirlem15  33554  mbfposadd  33587  ftc1anclem3  33617  rrnmval  33757  dvhopaddN  36720  pellex  37716  rmxfval  37785  rmyfval  37786  qirropth  37790  rmxycomplete  37799  jm2.15nn0  37887  rmxdioph  37900  expdiophlem2  37906  mendvsca  38078  deg1mhm  38102  addrval  38987  subrval  38988  fmulcl  40131  fmuldfeqlem1  40132  idmgmhm  42113  resmgmhm  42123  rhmval  42244  offval0  42624