Theorem oveqdr 7468

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570  (class class class)co 7440

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-uni 4871  df-br 5107  df-iota 6509  df-fv 6563  df-ov 7443

This theorem is used by:  fullresc  18052  fucpropd  18181  resssetc  18293  resscatc  18310  issstrmgm  18857  gsumpropd  18893  issubmgm2  18918  grpsubpropd  19281  sylow2blem2  19862  isrngd  20422  prdsrngd  20425  isringd  20549  prdsringd  20577  prdscrngd  20578  prds1  20579  rnghmval  20697  pwsco1rhm  20768  pwsco2rhm  20769  pwsdiagrhm  20886  rnghmsubcsetclem1  20910  rnghmsubcsetclem2  20911  rngcifuestrc  20918  rhmsubcsetclem1  20939  rhmsubcsetclem2  20940  rhmsubcrngclem1  20945  rhmsubcrngclem2  20946  isdomn  20984  primefld  21089  sraring  21488  sralmod  21489  sralmod0  21490  issubrgd  21491  znzrh  21875  zncrng  21877  phlssphl  21992  opsrcrng  22395  opsrassa  22396  ply1lss  22541  ply1subrg  22542  opsr0  22563  opsr1  22564  subrgply1  22577  opsrring  22589  opsrlmod  22590  ply1mpl0  22601  ply1mpl1  22603  ply1ascl  22604  coe1tm  22619  evls1rhm  22667  evl1rhm  22677  evl1expd  22690  evls1maplmhm  22722  mat0  22759  matinvg  22760  matlmod  22771  scmatsrng1  22865  1mavmul  22890  mat2pmatmul  23076  ressprdsds  24717  nmpropd  24940  tng0  24989  tngngp2  24998  tnggrpr  25001  tngnrg  25020  sranlm  25030  pi1addval  25396  cvsi  25478  tcphphl  25575  abvpropd2  33593  resv0g  33966  resvcmn  33968  sra1r  34280  sradrng  34281  sraidom  34282  srasubrg  34283  srapwov  34288  drgextlsp  34293  tnglvec  34311  tngdim  34312  matdim  34314  fedgmullem2  34329  fldextrspunfld  34375  zhmnrg  34664  prdsbnd  38918  prdstotbnd  38919  prdsbnd2  38920  erngdvlem3  42238  erngdvlem3-rN  42246  hlhils0  43193  hlhils1N  43194  hlhillvec  43199  hlhildrng  43200  hlhil0  43203  hlhillsm  43204  zndvdchrrhm  43214  isprimroot  43334  primrootsunit1  43338  mendval  44371  mnring0gd  45409  mnringlmodd  45414  grpgimcanon  46121  ovmpt4d  50179  upfval  50495  prcofvalg  50714