Theorem oveqdr 7390

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 7379	. 2 ⊢ (𝜑 → (𝑥𝐹𝑦) = (𝑥𝐺𝑦))
3	2	adantr 481	1 ⊢ ((𝜑 ∧ 𝜓) → (𝑥𝐹𝑦) = (𝑥𝐺𝑦))

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541  (class class class)co 7362

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930  df-uni 4871  df-br 5111  df-iota 6453  df-fv 6509  df-ov 7365

This theorem is referenced by:  fullresc  17751  fucpropd  17880  resssetc  17992  resscatc  18009  issstrmgm  18522  gsumpropd  18547  grpsubpropd  18866  sylow2blem2  19417  isringd  20023  prdsringd  20050  prdscrngd  20051  prds1  20052  pwsco1rhm  20188  pwsco2rhm  20189  pwsdiagrhm  20306  primefld  20328  sralmod  20715  sralmod0  20716  issubrngd2  20717  isdomn  20801  znzrh  20986  zncrng  20988  phlssphl  21100  sraassa  21310  opsrcrng  21503  opsrassa  21504  ply1lss  21604  ply1subrg  21605  opsr0  21626  opsr1  21627  subrgply1  21641  opsrring  21653  opsrlmod  21654  ply1mpl0  21663  ply1mpl1  21665  ply1ascl  21666  coe1tm  21681  evls1rhm  21725  evl1rhm  21735  evl1expd  21748  mat0  21803  matinvg  21804  matlmod  21815  scmatsrng1  21909  1mavmul  21934  mat2pmatmul  22117  ressprdsds  23761  nmpropd  23987  tng0  24039  tngngp2  24053  tnggrpr  24056  tngnrg  24075  sranlm  24085  pi1addval  24448  cvsi  24530  tcphphl  24628  abvpropd2  31889  resv0g  32203  resvcmn  32205  sra1r  32369  sraring  32370  sradrng  32371  srasubrg  32372  drgextlsp  32379  tnglvec  32394  tngdim  32395  matdim  32397  fedgmullem2  32412  evls1maplmhm  32456  zhmnrg  32637  prdsbnd  36325  prdstotbnd  36326  prdsbnd2  36327  erngdvlem3  39526  erngdvlem3-rN  39534  hlhils0  40485  hlhils1N  40486  hlhillvec  40491  hlhildrng  40492  hlhil0  40495  hlhillsm  40496  mendval  41568  mnring0gd  42621  mnringlmodd  42628  issubmgm2  46204  rnghmval  46309  lidlmmgm  46343  rnghmsubcsetclem1  46393  rnghmsubcsetclem2  46394  rngcifuestrc  46415  rhmsubcsetclem1  46439  rhmsubcsetclem2  46440  rhmsubcrngclem1  46445  rhmsubcrngclem2  46446