Theorem oveqdr 7388

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1548  (class class class)co 7360

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-ss 3902  df-uni 4842  df-br 5076  df-iota 6445  df-fv 6497  df-ov 7363

This theorem is referenced by:  fullresc  17813  fucpropd  17942  resssetc  18054  resscatc  18071  issstrmgm  18616  gsumpropd  18641  issubmgm2  18666  grpsubpropd  19016  sylow2blem2  19591  isrngd  20149  prdsrngd  20152  isringd  20267  prdsringd  20295  prdscrngd  20296  prds1  20297  rnghmval  20415  pwsco1rhm  20477  pwsco2rhm  20478  pwsdiagrhm  20583  rnghmsubcsetclem1  20607  rnghmsubcsetclem2  20608  rngcifuestrc  20615  rhmsubcsetclem1  20636  rhmsubcsetclem2  20637  rhmsubcrngclem1  20642  rhmsubcrngclem2  20643  isdomn  20681  primefld  20781  sraring  21180  sralmod  21181  sralmod0  21182  issubrgd  21183  znzrh  21521  zncrng  21523  phlssphl  21638  opsrcrng  22039  opsrassa  22040  ply1lss  22185  ply1subrg  22186  opsr0  22207  opsr1  22208  subrgply1  22221  opsrring  22233  opsrlmod  22234  ply1mpl0  22245  ply1mpl1  22247  ply1ascl  22248  coe1tm  22263  evls1rhm  22312  evl1rhm  22322  evl1expd  22335  evls1maplmhm  22367  mat0  22404  matinvg  22405  matlmod  22416  scmatsrng1  22510  1mavmul  22535  mat2pmatmul  22718  ressprdsds  24358  nmpropd  24581  tng0  24630  tngngp2  24639  tnggrpr  24642  tngnrg  24661  sranlm  24671  pi1addval  25037  cvsi  25119  tcphphl  25216  abvpropd2  33048  resv0g  33425  resvcmn  33427  sra1r  33777  sradrng  33778  sraidom  33779  srasubrg  33780  srapwov  33785  drgextlsp  33790  tnglvec  33808  tngdim  33809  matdim  33811  fedgmullem2  33826  fldextrspunfld  33872  zhmnrg  34161  prdsbnd  38175  prdstotbnd  38176  prdsbnd2  38177  erngdvlem3  41497  erngdvlem3-rN  41505  hlhils0  42452  hlhils1N  42453  hlhillvec  42458  hlhildrng  42459  hlhil0  42462  hlhillsm  42463  zndvdchrrhm  42473  isprimroot  42593  primrootsunit1  42597  mendval  43639  mnring0gd  44680  mnringlmodd  44685  ovmpt4d  49369  upfval  49680  prcofvalg  49880