Theorem oveqan12d 6568

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

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475  (class class class)co 6549

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552

This theorem is referenced by:  oveqan12rd  6569  offval  6802  offval3  7053  odi  7546  omopth2  7551  oeoa  7564  ecovdi  7743  ackbij1lem9  8933  alephadd  9278  distrpi  9599  addpipq  9638  mulpipq  9641  lterpq  9671  reclem3pr  9750  1idsr  9798  mulcnsr  9836  mulid1  9916  1re  9918  mul02  10093  addcom  10101  mulsub  10352  mulsub2  10353  muleqadd  10550  divmuldiv  10604  div2sub  10729  addltmul  11145  xnegdi  11950  xadddilem  11996  fzsubel  12248  fzoval  12340  seqid3  12707  mulexp  12761  sqdiv  12790  hashdom  13029  hashun  13032  ccatfval  13211  splcl  13354  crim  13703  readd  13714  remullem  13716  imadd  13722  cjadd  13729  cjreim  13748  sqrtmul  13848  sqabsadd  13870  sqabssub  13871  absmul  13882  abs2dif  13920  binom  14401  binomfallfac  14611  sinadd  14733  cosadd  14734  dvds2ln  14852  sadcaddlem  15017  bezoutlem4  15097  bezout  15098  absmulgcd  15104  gcddiv  15106  bezoutr1  15120  lcmgcd  15158  lcmfass  15197  nn0gcdsq  15298  crth  15321  pythagtriplem1  15359  pcqmul  15396  4sqlem4a  15493  4sqlem4  15494  prdsplusgval  15956  prdsmulrval  15958  prdsdsval  15961  prdsvscaval  15962  xpsfval  16050  xpsval  16055  idmhm  17167  0mhm  17181  resmhm  17182  prdspjmhm  17190  pwsdiagmhm  17192  gsumws2  17202  frmdup1  17224  eqgval  17466  idghm  17498  resghm  17499  mulgmhm  18056  mulgghm  18057  srglmhm  18358  srgrmhm  18359  ringlghm  18427  ringrghm  18428  gsumdixp  18432  isrhm  18544  issrngd  18684  lmodvsghm  18747  pwssplit2  18881  asclghm  19159  psrmulfval  19206  evlslem4  19329  mpfrcl  19339  xrsdsval  19609  expmhm  19634  expghm  19663  mulgghm2  19664  mulgrhm  19665  cygznlem3  19737  mamuval  20011  mamufv  20012  mvmulval  20168  mndifsplit  20261  mat2pmatmul  20355  decpmatmul  20396  fmval  21557  fmf  21559  flffval  21603  divcn  22479  rescncf  22508  htpyco1  22585  tchcph  22844  volun  23120  dyadval  23166  dvlip  23560  ftc1a  23604  ftc2ditglem  23612  tdeglem3  23623  q1pval  23717  reefgim  24008  relogoprlem  24141  eflogeq  24152  zetacvg  24541  lgsdir2  24855  lgsdchr  24880  brbtwn2  25585  ax5seglem4  25612  axeuclid  25643  axcontlem2  25645  axcontlem4  25647  axcontlem8  25651  numclwlk1lem2fo  26622  ipasslem11  27079  hhssnv  27505  mayete3i  27971  idunop  28221  idhmop  28225  0lnfn  28228  lnopmi  28243  lnophsi  28244  lnopcoi  28246  hmops  28263  hmopm  28264  nlelshi  28303  cnlnadjlem2  28311  kbass6  28364  strlem3a  28495  hstrlem3a  28503  bhmafibid1  28975  mndpluscn  29300  xrge0iifhom  29311  rezh  29343  probdsb  29811  rescon  30482  iscvm  30495  fwddifnval  31440  bj-bary1  32339  poimirlem15  32594  mbfposadd  32627  ftc1anclem3  32657  rrnmval  32797  dvhopaddN  35421  pellex  36417  rmxfval  36486  rmyfval  36487  qirropth  36491  rmxycomplete  36500  jm2.15nn0  36588  rmxdioph  36601  expdiophlem2  36607  mendvsca  36780  deg1mhm  36804  addrval  37691  subrval  37692  fmulcl  38648  fmuldfeqlem1  38649  av-numclwlk1lem2fo  41525  idmgmhm  41578  resmgmhm  41588  rhmval  41709  offval0  42093