Theorem oveqdr 7418

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  (class class class)co 7390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-ss 3934  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393

This theorem is referenced by:  fullresc  17820  fucpropd  17949  resssetc  18061  resscatc  18078  issstrmgm  18587  gsumpropd  18612  issubmgm2  18637  grpsubpropd  18984  sylow2blem2  19558  isrngd  20089  prdsrngd  20092  isringd  20207  prdsringd  20237  prdscrngd  20238  prds1  20239  rnghmval  20356  pwsco1rhm  20418  pwsco2rhm  20419  pwsdiagrhm  20523  rnghmsubcsetclem1  20547  rnghmsubcsetclem2  20548  rngcifuestrc  20555  rhmsubcsetclem1  20576  rhmsubcsetclem2  20577  rhmsubcrngclem1  20582  rhmsubcrngclem2  20583  isdomn  20621  primefld  20721  sraring  21100  sralmod  21101  sralmod0  21102  issubrgd  21103  znzrh  21459  zncrng  21461  phlssphl  21575  sraassaOLD  21786  opsrcrng  21973  opsrassa  21974  ply1lss  22088  ply1subrg  22089  opsr0  22110  opsr1  22111  subrgply1  22124  opsrring  22136  opsrlmod  22137  ply1mpl0  22148  ply1mpl1  22150  ply1ascl  22151  coe1tm  22166  evls1rhm  22216  evl1rhm  22226  evl1expd  22239  evls1maplmhm  22271  mat0  22311  matinvg  22312  matlmod  22323  scmatsrng1  22417  1mavmul  22442  mat2pmatmul  22625  ressprdsds  24266  nmpropd  24489  tng0  24538  tngngp2  24547  tnggrpr  24550  tngnrg  24569  sranlm  24579  pi1addval  24955  cvsi  25037  tcphphl  25134  abvpropd2  32894  resv0g  33317  resvcmn  33319  sra1r  33584  sradrng  33585  sraidom  33586  srasubrg  33587  drgextlsp  33596  tnglvec  33615  tngdim  33616  matdim  33618  fedgmullem2  33633  fldextrspunfld  33678  zhmnrg  33962  prdsbnd  37794  prdstotbnd  37795  prdsbnd2  37796  erngdvlem3  40991  erngdvlem3-rN  40999  hlhils0  41946  hlhils1N  41947  hlhillvec  41952  hlhildrng  41953  hlhil0  41956  hlhillsm  41957  zndvdchrrhm  41967  isprimroot  42088  primrootsunit1  42092  mendval  43175  mnring0gd  44217  mnringlmodd  44222  ovmpt4d  48857  upfval  49169  prcofvalg  49369