Theorem oveqan12d 7365

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541  (class class class)co 7346

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-iota 6437  df-fv 6489  df-ov 7349

This theorem is referenced by:  oveqan12rd  7366  offval  7619  offval3  7914  odi  8494  omopth2  8499  oeoa  8512  ecovdi  8749  ackbij1lem9  10118  distrpi  10789  addpipq  10828  mulpipq  10831  lterpq  10861  reclem3pr  10940  1idsr  10989  mulcnsr  11027  mulrid  11110  1re  11112  mul02  11291  addcom  11299  mulsub  11560  mulsub2  11561  muleqadd  11761  divmuldiv  11821  div2sub  11946  addltmul  12357  xnegdi  13147  xadddilem  13193  fzsubel  13460  fzoval  13560  seqid3  13953  mulexp  14008  sqdiv  14028  hashdom  14286  hashun  14289  ccatfval  14480  splcl  14659  crim  15022  readd  15033  remullem  15035  imadd  15041  cjadd  15048  cjreim  15067  sqrtmul  15166  sqabsadd  15189  sqabssub  15190  absmul  15201  abs2dif  15240  bhmafibid1  15375  binom  15737  binomfallfac  15948  sinadd  16073  cosadd  16074  dvds2ln  16200  sadcaddlem  16368  bezoutlem4  16453  bezout  16454  absmulgcd  16460  gcddiv  16462  bezoutr1  16480  lcmgcd  16518  lcmfass  16557  nn0gcdsq  16663  crth  16689  pythagtriplem1  16728  pcqmul  16765  4sqlem4a  16863  4sqlem4  16864  prdsplusgval  17377  prdsmulrval  17379  prdsdsval  17382  prdsvscaval  17383  idmgmhm  18609  resmgmhm  18619  idmhm  18703  0mhm  18727  resmhm  18728  prdspjmhm  18737  pwsdiagmhm  18739  gsumws2  18750  frmdup1  18772  eqgval  19089  idghm  19143  resghm  19144  mulgmhm  19739  mulgghm  19740  srglmhm  20139  srgrmhm  20140  ringlghm  20230  ringrghm  20231  gsumdixp  20237  isrhm  20396  rhmval  20415  issrngd  20770  lmodvsghm  20856  pwssplit2  20994  xrsdsval  21347  expmhm  21373  expghm  21412  mulgghm2  21413  mulgrhm  21414  pzriprnglem4  21421  cygznlem3  21506  asclghm  21820  psrmulfval  21880  evlslem4  22011  mpfrcl  22020  mamuval  22308  mamufv  22309  mvmulval  22458  mndifsplit  22551  mat2pmatmul  22646  decpmatmul  22687  fmval  23858  fmf  23860  flffval  23904  divcnOLD  24784  divcn  24786  rescncf  24817  htpyco1  24904  tcphcph  25164  rrxdsfival  25340  ehl2eudisval  25350  volun  25473  dyadval  25520  dvlip  25925  ftc1a  25971  ftc2ditglem  25979  tdeglem3  25991  q1pval  26087  reefgim  26387  relogoprlem  26527  eflogeq  26538  zetacvg  26952  lgsdir2  27268  lgsdchr  27293  2sq2  27371  2sqnn0  27376  negsdi  27992  brbtwn2  28883  ax5seglem4  28910  axeuclid  28941  axcontlem2  28943  axcontlem4  28945  axcontlem8  28949  clwwlknccat  30043  ex-fpar  30442  ipasslem11  30820  hhssnv  31244  mayete3i  31708  idunop  31958  idhmop  31962  0lnfn  31965  lnopmi  31980  lnophsi  31981  lnopcoi  31983  hmops  32000  hmopm  32001  nlelshi  32040  cnlnadjlem2  32048  kbass6  32101  strlem3a  32232  hstrlem3a  32240  elrgspnlem2  33210  mndpluscn  33939  xrge0iifhom  33950  rezh  33982  probdsb  34435  resconn  35290  iscvm  35303  satfdmlem  35412  satffunlem1lem1  35446  satffunlem2lem1  35448  fwddifnval  36207  bj-bary1  37356  poimirlem15  37674  mbfposadd  37706  ftc1anclem3  37734  rrnmval  37867  dvhopaddN  41212  nnadddir  42362  cnreeu  42582  prjcrvfval  42723  pellex  42927  rmxfval  42996  rmyfval  42997  qirropth  43000  rmxycomplete  43009  jm2.15nn0  43095  rmxdioph  43108  expdiophlem2  43114  mendvsca  43279  deg1mhm  43292  mnringmulrvald  44319  addrval  44557  subrval  44558  fmulcl  45680  fmuldfeqlem1  45681  line  48832  itsclc0xyqsolr  48869