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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542  (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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-uni 4852  df-br 5087  df-iota 6450  df-fv 6502  df-ov 7365

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  20474  pwsco2rhm  20475  pwsdiagrhm  20579  rnghmsubcsetclem1  20603  rnghmsubcsetclem2  20604  rngcifuestrc  20611  rhmsubcsetclem1  20632  rhmsubcsetclem2  20633  rhmsubcrngclem1  20638  rhmsubcrngclem2  20639  isdomn  20677  primefld  20777  sraring  21177  sralmod  21178  sralmod0  21179  issubrgd  21180  znzrh  21536  zncrng  21538  phlssphl  21653  opsrcrng  22051  opsrassa  22052  ply1lss  22174  ply1subrg  22175  opsr0  22196  opsr1  22197  subrgply1  22210  opsrring  22222  opsrlmod  22223  ply1mpl0  22234  ply1mpl1  22236  ply1ascl  22237  coe1tm  22252  evls1rhm  22301  evl1rhm  22311  evl1expd  22324  evls1maplmhm  22356  mat0  22396  matinvg  22397  matlmod  22408  scmatsrng1  22502  1mavmul  22527  mat2pmatmul  22710  ressprdsds  24350  nmpropd  24573  tng0  24622  tngngp2  24631  tnggrpr  24634  tngnrg  24653  sranlm  24663  pi1addval  25029  cvsi  25111  tcphphl  25208  abvpropd2  33044  resv0g  33417  resvcmn  33419  sra1r  33744  sradrng  33745  sraidom  33746  srasubrg  33747  srapwov  33752  drgextlsp  33757  tnglvec  33776  tngdim  33777  matdim  33779  fedgmullem2  33794  fldextrspunfld  33840  zhmnrg  34129  prdsbnd  38134  prdstotbnd  38135  prdsbnd2  38136  erngdvlem3  41456  erngdvlem3-rN  41464  hlhils0  42411  hlhils1N  42412  hlhillvec  42417  hlhildrng  42418  hlhil0  42421  hlhillsm  42422  zndvdchrrhm  42432  isprimroot  42552  primrootsunit1  42556  mendval  43631  mnring0gd  44672  mnringlmodd  44677  ovmpt4d  49358  upfval  49669  prcofvalg  49869