Theorem oveqan12d 7467

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537  (class class class)co 7448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451

This theorem is referenced by:  oveqan12rd  7468  offval  7723  offval3  8023  odi  8635  omopth2  8640  oeoa  8653  ecovdi  8883  ackbij1lem9  10296  distrpi  10967  addpipq  11006  mulpipq  11009  lterpq  11039  reclem3pr  11118  1idsr  11167  mulcnsr  11205  mulrid  11288  1re  11290  mul02  11468  addcom  11476  mulsub  11733  mulsub2  11734  muleqadd  11934  divmuldiv  11994  div2sub  12119  addltmul  12529  xnegdi  13310  xadddilem  13356  fzsubel  13620  fzoval  13717  seqid3  14097  mulexp  14152  sqdiv  14171  hashdom  14428  hashun  14431  ccatfval  14621  splcl  14800  crim  15164  readd  15175  remullem  15177  imadd  15183  cjadd  15190  cjreim  15209  sqrtmul  15308  sqabsadd  15331  sqabssub  15332  absmul  15343  abs2dif  15381  bhmafibid1  15514  binom  15878  binomfallfac  16089  sinadd  16212  cosadd  16213  dvds2ln  16337  sadcaddlem  16503  bezoutlem4  16589  bezout  16590  absmulgcd  16596  gcddiv  16598  bezoutr1  16616  lcmgcd  16654  lcmfass  16693  nn0gcdsq  16799  crth  16825  pythagtriplem1  16863  pcqmul  16900  4sqlem4a  16998  4sqlem4  16999  prdsplusgval  17533  prdsmulrval  17535  prdsdsval  17538  prdsvscaval  17539  idmgmhm  18739  resmgmhm  18749  idmhm  18830  0mhm  18854  resmhm  18855  prdspjmhm  18864  pwsdiagmhm  18866  gsumws2  18877  frmdup1  18899  eqgval  19217  idghm  19271  resghm  19272  mulgmhm  19869  mulgghm  19870  srglmhm  20248  srgrmhm  20249  ringlghm  20335  ringrghm  20336  gsumdixp  20342  isrhm  20504  rhmval  20526  issrngd  20878  lmodvsghm  20943  pwssplit2  21082  xrsdsval  21451  expmhm  21477  expghm  21509  mulgghm2  21510  mulgrhm  21511  pzriprnglem4  21518  cygznlem3  21611  asclghm  21926  psrmulfval  21986  evlslem4  22123  mpfrcl  22132  mamuval  22418  mamufv  22419  mvmulval  22570  mndifsplit  22663  mat2pmatmul  22758  decpmatmul  22799  fmval  23972  fmf  23974  flffval  24018  divcnOLD  24909  divcn  24911  rescncf  24942  htpyco1  25029  tcphcph  25290  rrxdsfival  25466  ehl2eudisval  25476  volun  25599  dyadval  25646  dvlip  26052  ftc1a  26098  ftc2ditglem  26106  tdeglem3  26118  q1pval  26214  reefgim  26512  relogoprlem  26651  eflogeq  26662  zetacvg  27076  lgsdir2  27392  lgsdchr  27417  2sq2  27495  2sqnn0  27500  negsdi  28100  brbtwn2  28938  ax5seglem4  28965  axeuclid  28996  axcontlem2  28998  axcontlem4  29000  axcontlem8  29004  clwwlknccat  30095  ex-fpar  30494  ipasslem11  30872  hhssnv  31296  mayete3i  31760  idunop  32010  idhmop  32014  0lnfn  32017  lnopmi  32032  lnophsi  32033  lnopcoi  32035  hmops  32052  hmopm  32053  nlelshi  32092  cnlnadjlem2  32100  kbass6  32153  strlem3a  32284  hstrlem3a  32292  mndpluscn  33872  xrge0iifhom  33883  rezh  33917  probdsb  34387  resconn  35214  iscvm  35227  satfdmlem  35336  satffunlem1lem1  35370  satffunlem2lem1  35372  fwddifnval  36127  bj-bary1  37278  poimirlem15  37595  mbfposadd  37627  ftc1anclem3  37655  rrnmval  37788  dvhopaddN  41071  nnadddir  42259  cnreeu  42446  prjcrvfval  42586  pellex  42791  rmxfval  42860  rmyfval  42861  qirropth  42864  rmxycomplete  42874  jm2.15nn0  42960  rmxdioph  42973  expdiophlem2  42979  mendvsca  43148  deg1mhm  43161  mnringmulrvald  44196  addrval  44435  subrval  44436  fmulcl  45502  fmuldfeqlem1  45503  line  48466  itsclc0xyqsolr  48503