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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542  (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 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 3443  df-ss 3919  df-uni 4865  df-br 5100  df-iota 6449  df-fv 6501  df-ov 7363

This theorem is referenced by:  fullresc  17779  fucpropd  17908  resssetc  18020  resscatc  18037  issstrmgm  18582  gsumpropd  18607  issubmgm2  18632  grpsubpropd  18979  sylow2blem2  19554  isrngd  20112  prdsrngd  20115  isringd  20230  prdsringd  20260  prdscrngd  20261  prds1  20262  rnghmval  20380  pwsco1rhm  20439  pwsco2rhm  20440  pwsdiagrhm  20544  rnghmsubcsetclem1  20568  rnghmsubcsetclem2  20569  rngcifuestrc  20576  rhmsubcsetclem1  20597  rhmsubcsetclem2  20598  rhmsubcrngclem1  20603  rhmsubcrngclem2  20604  isdomn  20642  primefld  20742  sraring  21142  sralmod  21143  sralmod0  21144  issubrgd  21145  znzrh  21501  zncrng  21503  phlssphl  21618  sraassaOLD  21829  opsrcrng  22018  opsrassa  22019  ply1lss  22141  ply1subrg  22142  opsr0  22163  opsr1  22164  subrgply1  22177  opsrring  22189  opsrlmod  22190  ply1mpl0  22201  ply1mpl1  22203  ply1ascl  22204  coe1tm  22219  evls1rhm  22270  evl1rhm  22280  evl1expd  22293  evls1maplmhm  22325  mat0  22365  matinvg  22366  matlmod  22377  scmatsrng1  22471  1mavmul  22496  mat2pmatmul  22679  ressprdsds  24319  nmpropd  24542  tng0  24591  tngngp2  24600  tnggrpr  24603  tngnrg  24622  sranlm  24632  pi1addval  25008  cvsi  25090  tcphphl  25187  abvpropd2  33049  resv0g  33421  resvcmn  33423  sra1r  33739  sradrng  33740  sraidom  33741  srasubrg  33742  srapwov  33747  drgextlsp  33752  tnglvec  33771  tngdim  33772  matdim  33774  fedgmullem2  33789  fldextrspunfld  33835  zhmnrg  34124  prdsbnd  37996  prdstotbnd  37997  prdsbnd2  37998  erngdvlem3  41318  erngdvlem3-rN  41326  hlhils0  42273  hlhils1N  42274  hlhillvec  42279  hlhildrng  42280  hlhil0  42283  hlhillsm  42284  zndvdchrrhm  42294  isprimroot  42415  primrootsunit1  42419  mendval  43488  mnring0gd  44529  mnringlmodd  44534  ovmpt4d  49177  upfval  49488  prcofvalg  49688