Theorem oveqdr 7178

Description: Equality of two operations for any two operands. Useful in proofs using *propd theorems. (Contributed by Mario Carneiro, 29-Jun-2015.)

Hypothesis

Ref	Expression
oveqdr.1	⊢ (𝜑 → 𝐹 = 𝐺)

Assertion

Ref	Expression
oveqdr	⊢ ((𝜑 ∧ 𝜓) → (𝑥𝐹𝑦) = (𝑥𝐺𝑦))

Proof of Theorem oveqdr

Step	Hyp	Ref	Expression
1		oveqdr.1	. . 3 ⊢ (𝜑 → 𝐹 = 𝐺)
2	1	oveqd 7167	. 2 ⊢ (𝜑 → (𝑥𝐹𝑦) = (𝑥𝐺𝑦))
3	2	adantr 484	1 ⊢ ((𝜑 ∧ 𝜓) → (𝑥𝐹𝑦) = (𝑥𝐺𝑦))

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538  (class class class)co 7150

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3865  df-ss 3875  df-uni 4799  df-br 5033  df-iota 6294  df-fv 6343  df-ov 7153

This theorem is referenced by:  fullresc  17180  fucpropd  17306  resssetc  17418  resscatc  17431  issstrmgm  17929  gsumpropd  17954  grpsubpropd  18271  sylow2blem2  18813  isringd  19406  prdsringd  19433  prdscrngd  19434  prds1  19435  pwsco1rhm  19561  pwsco2rhm  19562  pwsdiagrhm  19637  primefld  19652  sralmod  20027  sralmod0  20028  issubrngd2  20029  isdomn  20135  znzrh  20310  zncrng  20312  phlssphl  20424  sraassa  20632  opsrcrng  20819  opsrassa  20820  ply1lss  20920  ply1subrg  20921  opsr0  20942  opsr1  20943  subrgply1  20957  opsrring  20969  opsrlmod  20970  ply1mpl0  20979  ply1mpl1  20981  ply1ascl  20982  coe1tm  20997  evls1rhm  21041  evl1rhm  21051  evl1expd  21064  mat0  21117  matinvg  21118  matlmod  21129  scmatsrng1  21223  1mavmul  21248  mat2pmatmul  21431  ressprdsds  23073  nmpropd  23296  tng0  23345  tngngp2  23354  tnggrpr  23357  tngnrg  23376  sranlm  23386  pi1addval  23749  cvsi  23831  tcphphl  23927  istrkgc  26347  istrkgb  26348  abvpropd2  30761  resv0g  31061  resvcmn  31063  sra1r  31192  sraring  31193  sradrng  31194  srasubrg  31195  drgextlsp  31202  tnglvec  31216  tngdim  31217  matdim  31219  fedgmullem2  31232  zhmnrg  31436  prdsbnd  35511  prdstotbnd  35512  prdsbnd2  35513  erngdvlem3  38566  erngdvlem3-rN  38574  hlhils0  39521  hlhils1N  39522  hlhillvec  39527  hlhildrng  39528  hlhil0  39531  hlhillsm  39532  mendval  40500  mnring0gd  41302  mnringlmodd  41307  issubmgm2  44777  rnghmval  44882  lidlmmgm  44916  rnghmsubcsetclem1  44966  rnghmsubcsetclem2  44967  rngcifuestrc  44988  rhmsubcsetclem1  45012  rhmsubcsetclem2  45013  rhmsubcrngclem1  45018  rhmsubcrngclem2  45019