Theorem oveqan12d 7462

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570  (class class class)co 7443

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6512  df-fv 6566  df-ov 7446

This theorem is used by:  oveqan12rd  7463  offval  7726  offval3  8018  odi  8615  omopth2  8620  oeoa  8634  ecovdi  8874  ackbij1lem9  10332  distrpi  11010  addpipq  11049  mulpipq  11052  lterpq  11082  reclem3pr  11161  1idsr  11210  mulcnsr  11248  mulrid  11333  1re  11335  mul02  11515  addcom  11523  mulsub  11786  mulsub2  11787  muleqadd  11987  divmuldiv  12044  div2sub  12169  nnadddir  12421  addltmul  12609  xnegdi  13405  xadddilem  13451  fzsubel  13721  fzoval  13821  seqid3  14216  mulexp  14271  sqdiv  14291  hashdom  14550  hashun  14553  ccatfval  14745  splcl  14929  crim  15311  readd  15322  remullem  15324  imadd  15330  cjadd  15337  cjreim  15356  sqrtmul  15455  sqabsadd  15478  sqabssub  15479  absmul  15490  abs2dif  15529  bhmafibid1  15664  binom  16028  binomfallfac  16236  sinadd  16361  cosadd  16362  dvds2ln  16488  sadcaddlem  16656  bezoutlem4  16744  bezout  16745  absmulgcd  16751  gcddiv  16753  bezoutr1  16773  lcmgcd  16811  lcmfass  16850  nn0gcdsq  16957  crth  16984  pythagtriplem1  17023  pcqmul  17060  4sqlem4a  17158  4sqlem4  17159  prdsplusgval  17673  prdsmulrval  17675  prdsdsval  17678  prdsvscaval  17679  idmgmhm  18919  resmgmhm  18929  idmhm  19019  0mhm  19044  resmhm  19045  prdspjmhm  19054  pwsdiagmhm  19056  gsumws2  19067  frmdup1  19089  eqgval  19418  idghm  19474  resghm  19475  mulgmhm  20071  mulgghm  20072  srglmhm  20477  srgrmhm  20478  ringlghm  20573  ringrghm  20574  gsumdixp  20578  isrhm  20739  rhmval  20768  issrngd  21142  lmodvsghm  21228  pwssplit2  21365  xrsdsval  21747  expmhm  21772  expghm  21811  mulgghm2  21812  mulgrhm  21813  pzriprnglem4  21820  cygznlem3  21905  asclghm  22220  psrmulfval  22281  evlslem4  22415  mpfrcl  22424  mamuval  22738  mamufv  22739  mvmulval  22888  mndifsplit  22981  mat2pmatmul  23079  decpmatmul  23120  fmval  24292  fmf  24294  flffval  24338  divcn  25219  rescncf  25248  htpyco1  25329  tcphcph  25588  rrxdsfival  25764  ehl2eudisval  25774  volun  25896  dyadval  25943  dvlip  26343  ftc1a  26387  ftc2ditglem  26395  tdeglem3  26407  q1pval  26503  reefgim  26807  relogoprlem  26949  eflogeq  26960  zetacvg  27372  lgsdir2  27687  lgsdchr  27712  2sq2  27790  2sqnn0  27795  negsdi  28466  brbtwn2  29513  ax5seglem4  29540  axeuclid  29571  axcontlem2  29573  axcontlem4  29575  axcontlem8  29579  clwwlknccat  30684  ex-fpar  31093  ipasslem11  31472  hhssnv  31896  mayete3i  32360  idunop  32610  idhmop  32614  0lnfn  32617  lnopmi  32632  lnophsi  32633  lnopcoi  32635  hmops  32652  hmopm  32653  nlelshi  32692  cnlnadjlem2  32700  kbass6  32753  strlem3a  32884  hstrlem3a  32892  elrgspnlem2  33874  mndpluscn  34628  xrge0iifhom  34639  rezh  34671  probdsb  35124  resconn  36178  iscvm  36191  satfdmlem  36300  satffunlem1lem1  36334  satffunlem2lem1  36336  fwddifnval  37106  bj-bary1  38425  poimirlem15  38745  mbfposadd  38777  ftc1anclem3  38805  rrnmval  38954  dvhopaddN  42363  cnreeu  43747  prjcrvfval  43860  pellex  44035  rmxfval  44104  rmyfval  44105  qirropth  44108  rmxycomplete  44117  jm2.15nn0  44203  rmxdioph  44216  expdiophlem2  44222  mendvsca  44381  deg1mhm  44394  mnringmulrvald  45417  addrval  45639  subrval  45640  hashnna  46204  fmulcl  46798  fmuldfeqlem1  46799  line  50050  itsclc0xyqsolr  50086  itscnhlinecirc02p  50102