Theorem oveqan12d 7415

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1561  (class class class)co 7396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3416  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5102  df-iota 6477  df-fv 6529  df-ov 7399

This theorem is referenced by:  oveqan12rd  7416  offval  7669  offval3  7963  odi  8548  omopth2  8553  oeoa  8567  ecovdi  8807  ackbij1lem9  10194  distrpi  10867  addpipq  10906  mulpipq  10909  lterpq  10939  reclem3pr  11018  1idsr  11067  mulcnsr  11105  mulrid  11190  1re  11192  mul02  11372  addcom  11380  mulsub  11641  mulsub2  11642  muleqadd  11842  divmuldiv  11902  div2sub  12027  nnadddir  12279  addltmul  12467  xnegdi  13261  xadddilem  13307  fzsubel  13575  fzoval  13675  seqid3  14069  mulexp  14124  sqdiv  14144  hashdom  14402  hashun  14405  ccatfval  14596  splcl  14775  crim  15152  readd  15163  remullem  15165  imadd  15171  cjadd  15178  cjreim  15197  sqrtmul  15296  sqabsadd  15319  sqabssub  15320  absmul  15331  abs2dif  15370  bhmafibid1  15505  binom  15870  binomfallfac  16081  sinadd  16206  cosadd  16207  dvds2ln  16333  sadcaddlem  16501  bezoutlem4  16586  bezout  16587  absmulgcd  16593  gcddiv  16595  bezoutr1  16613  lcmgcd  16651  lcmfass  16690  nn0gcdsq  16797  crth  16823  pythagtriplem1  16862  pcqmul  16899  4sqlem4a  16997  4sqlem4  16998  prdsplusgval  17512  prdsmulrval  17514  prdsdsval  17517  prdsvscaval  17518  idmgmhm  18745  resmgmhm  18755  idmhm  18839  0mhm  18863  resmhm  18864  prdspjmhm  18873  pwsdiagmhm  18875  gsumws2  18886  frmdup1  18908  eqgval  19228  idghm  19281  resghm  19282  mulgmhm  19877  mulgghm  19878  srglmhm  20281  srgrmhm  20282  ringlghm  20372  ringrghm  20373  gsumdixp  20377  isrhm  20537  rhmval  20559  issrngd  20911  lmodvsghm  20997  pwssplit2  21134  xrsdsval  21470  expmhm  21495  expghm  21534  mulgghm2  21535  mulgrhm  21536  pzriprnglem4  21543  cygznlem3  21628  asclghm  21941  psrmulfval  22002  evlslem4  22136  mpfrcl  22145  mamuval  22460  mamufv  22461  mvmulval  22610  mndifsplit  22703  mat2pmatmul  22798  decpmatmul  22839  fmval  24010  fmf  24012  flffval  24056  divcn  24937  rescncf  24966  htpyco1  25047  tcphcph  25306  rrxdsfival  25482  ehl2eudisval  25492  volun  25614  dyadval  25661  dvlip  26062  ftc1a  26106  ftc2ditglem  26114  tdeglem3  26126  q1pval  26222  reefgim  26520  relogoprlem  26663  eflogeq  26674  zetacvg  27086  lgsdir2  27401  lgsdchr  27426  2sq2  27504  2sqnn0  27509  negsdi  28150  brbtwn2  29113  ax5seglem4  29140  axeuclid  29171  axcontlem2  29173  axcontlem4  29175  axcontlem8  29179  clwwlknccat  30272  ex-fpar  30671  ipasslem11  31050  hhssnv  31474  mayete3i  31938  idunop  32188  idhmop  32192  0lnfn  32195  lnopmi  32210  lnophsi  32211  lnopcoi  32213  hmops  32230  hmopm  32231  nlelshi  32270  cnlnadjlem2  32278  kbass6  32331  strlem3a  32462  hstrlem3a  32470  elrgspnlem2  33430  mndpluscn  34225  xrge0iifhom  34236  rezh  34268  probdsb  34721  resconn  35601  iscvm  35614  satfdmlem  35723  satffunlem1lem1  35757  satffunlem2lem1  35759  fwddifnval  36518  bj-bary1  37809  poimirlem15  38139  mbfposadd  38171  ftc1anclem3  38199  rrnmval  38332  dvhopaddN  41743  cnreeu  43117  prjcrvfval  43218  pellex  43417  rmxfval  43486  rmyfval  43487  qirropth  43490  rmxycomplete  43499  jm2.15nn0  43585  rmxdioph  43598  expdiophlem2  43604  mendvsca  43769  deg1mhm  43782  mnringmulrvald  44808  addrval  45032  subrval  45033  fmulcl  46148  fmuldfeqlem1  46149  line  49345  itsclc0xyqsolr  49382