Theorem oveqan12d 6832

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

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1632  (class class class)co 6813

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-iota 6012  df-fv 6057  df-ov 6816

This theorem is referenced by:  oveqan12rd  6833  offval  7069  offval3  7327  odi  7828  omopth2  7833  oeoa  7846  ecovdi  8022  ackbij1lem9  9242  alephadd  9591  distrpi  9912  addpipq  9951  mulpipq  9954  lterpq  9984  reclem3pr  10063  1idsr  10111  mulcnsr  10149  mulid1  10229  1re  10231  mul02  10406  addcom  10414  mulsub  10665  mulsub2  10666  muleqadd  10863  divmuldiv  10917  div2sub  11042  addltmul  11460  xnegdi  12271  xadddilem  12317  fzsubel  12570  fzoval  12665  seqid3  13039  mulexp  13093  sqdiv  13122  hashdom  13360  hashun  13363  ccatfval  13545  splcl  13703  crim  14054  readd  14065  remullem  14067  imadd  14073  cjadd  14080  cjreim  14099  sqrtmul  14199  sqabsadd  14221  sqabssub  14222  absmul  14233  abs2dif  14271  binom  14761  binomfallfac  14971  sinadd  15093  cosadd  15094  dvds2ln  15216  sadcaddlem  15381  bezoutlem4  15461  bezout  15462  absmulgcd  15468  gcddiv  15470  bezoutr1  15484  lcmgcd  15522  lcmfass  15561  nn0gcdsq  15662  crth  15685  pythagtriplem1  15723  pcqmul  15760  4sqlem4a  15857  4sqlem4  15858  prdsplusgval  16335  prdsmulrval  16337  prdsdsval  16340  prdsvscaval  16341  xpsfval  16429  xpsval  16434  idmhm  17545  0mhm  17559  resmhm  17560  prdspjmhm  17568  pwsdiagmhm  17570  gsumws2  17580  frmdup1  17602  eqgval  17844  idghm  17876  resghm  17877  mulgmhm  18433  mulgghm  18434  srglmhm  18735  srgrmhm  18736  ringlghm  18804  ringrghm  18805  gsumdixp  18809  isrhm  18923  issrngd  19063  lmodvsghm  19126  pwssplit2  19262  asclghm  19540  psrmulfval  19587  evlslem4  19710  mpfrcl  19720  xrsdsval  19992  expmhm  20017  expghm  20046  mulgghm2  20047  mulgrhm  20048  cygznlem3  20120  mamuval  20394  mamufv  20395  mvmulval  20551  mndifsplit  20644  mat2pmatmul  20738  decpmatmul  20779  fmval  21948  fmf  21950  flffval  21994  divcn  22872  rescncf  22901  htpyco1  22978  tchcph  23236  volun  23513  dyadval  23560  dvlip  23955  ftc1a  23999  ftc2ditglem  24007  tdeglem3  24018  q1pval  24112  reefgim  24403  relogoprlem  24536  eflogeq  24547  zetacvg  24940  lgsdir2  25254  lgsdchr  25279  brbtwn2  25984  ax5seglem4  26011  axeuclid  26042  axcontlem2  26044  axcontlem4  26046  axcontlem8  26050  clwwlknccat  27194  ipasslem11  28004  hhssnv  28430  mayete3i  28896  idunop  29146  idhmop  29150  0lnfn  29153  lnopmi  29168  lnophsi  29169  lnopcoi  29171  hmops  29188  hmopm  29189  nlelshi  29228  cnlnadjlem2  29236  kbass6  29289  strlem3a  29420  hstrlem3a  29428  bhmafibid1  29953  mndpluscn  30281  xrge0iifhom  30292  rezh  30324  probdsb  30793  resconn  31535  iscvm  31548  fwddifnval  32576  bj-bary1  33473  poimirlem15  33737  mbfposadd  33770  ftc1anclem3  33800  rrnmval  33940  dvhopaddN  36905  pellex  37901  rmxfval  37970  rmyfval  37971  qirropth  37975  rmxycomplete  37984  jm2.15nn0  38072  rmxdioph  38085  expdiophlem2  38091  mendvsca  38263  deg1mhm  38287  addrval  39172  subrval  39173  fmulcl  40316  fmuldfeqlem1  40317  idmgmhm  42298  resmgmhm  42308  rhmval  42429  offval0  42809