Theorem oveqdr 7440

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   = wceq 1569  (class class class)co 7412

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-ss 3921  df-uni 4872  df-br 5109  df-iota 6492  df-fv 6544  df-ov 7415

This theorem is used by:  fullresc  17914  fucpropd  18043  resssetc  18155  resscatc  18172  issstrmgm  18717  gsumpropd  18742  issubmgm2  18767  grpsubpropd  19117  sylow2blem2  19697  isrngd  20257  prdsrngd  20260  isringd  20381  prdsringd  20409  prdscrngd  20410  prds1  20411  rnghmval  20529  pwsco1rhm  20600  pwsco2rhm  20601  pwsdiagrhm  20717  rnghmsubcsetclem1  20741  rnghmsubcsetclem2  20742  rngcifuestrc  20749  rhmsubcsetclem1  20770  rhmsubcsetclem2  20771  rhmsubcrngclem1  20776  rhmsubcrngclem2  20777  isdomn  20815  primefld  20919  sraring  21318  sralmod  21319  sralmod0  21320  issubrgd  21321  znzrh  21703  zncrng  21705  phlssphl  21820  opsrcrng  22221  opsrassa  22222  ply1lss  22367  ply1subrg  22368  opsr0  22389  opsr1  22390  subrgply1  22403  opsrring  22415  opsrlmod  22416  ply1mpl0  22427  ply1mpl1  22429  ply1ascl  22430  coe1tm  22445  evls1rhm  22493  evl1rhm  22503  evl1expd  22516  evls1maplmhm  22548  mat0  22585  matinvg  22586  matlmod  22597  scmatsrng1  22691  1mavmul  22716  mat2pmatmul  22899  ressprdsds  24539  nmpropd  24762  tng0  24811  tngngp2  24820  tnggrpr  24823  tngnrg  24842  sranlm  24852  pi1addval  25218  cvsi  25300  tcphphl  25397  abvpropd2  33294  resv0g  33667  resvcmn  33669  sra1r  33980  sradrng  33981  sraidom  33982  srasubrg  33983  srapwov  33988  drgextlsp  33993  tnglvec  34011  tngdim  34012  matdim  34014  fedgmullem2  34029  fldextrspunfld  34075  zhmnrg  34364  prdsbnd  38472  prdstotbnd  38473  prdsbnd2  38474  erngdvlem3  41792  erngdvlem3-rN  41800  hlhils0  42747  hlhils1N  42748  hlhillvec  42753  hlhildrng  42754  hlhil0  42757  hlhillsm  42758  zndvdchrrhm  42768  isprimroot  42888  primrootsunit1  42892  mendval  43934  mnring0gd  44973  mnringlmodd  44978  ovmpt4d  49671  upfval  49982  prcofvalg  50182