Theorem oveqdr 7386

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542  (class class class)co 7358

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-v 3441  df-ss 3917  df-uni 4863  df-br 5098  df-iota 6447  df-fv 6499  df-ov 7361

This theorem is referenced by:  fullresc  17777  fucpropd  17906  resssetc  18018  resscatc  18035  issstrmgm  18580  gsumpropd  18605  issubmgm2  18630  grpsubpropd  18977  sylow2blem2  19552  isrngd  20110  prdsrngd  20113  isringd  20228  prdsringd  20258  prdscrngd  20259  prds1  20260  rnghmval  20378  pwsco1rhm  20437  pwsco2rhm  20438  pwsdiagrhm  20542  rnghmsubcsetclem1  20566  rnghmsubcsetclem2  20567  rngcifuestrc  20574  rhmsubcsetclem1  20595  rhmsubcsetclem2  20596  rhmsubcrngclem1  20601  rhmsubcrngclem2  20602  isdomn  20640  primefld  20740  sraring  21140  sralmod  21141  sralmod0  21142  issubrgd  21143  znzrh  21499  zncrng  21501  phlssphl  21616  sraassaOLD  21827  opsrcrng  22016  opsrassa  22017  ply1lss  22139  ply1subrg  22140  opsr0  22161  opsr1  22162  subrgply1  22175  opsrring  22187  opsrlmod  22188  ply1mpl0  22199  ply1mpl1  22201  ply1ascl  22202  coe1tm  22217  evls1rhm  22268  evl1rhm  22278  evl1expd  22291  evls1maplmhm  22323  mat0  22363  matinvg  22364  matlmod  22375  scmatsrng1  22469  1mavmul  22494  mat2pmatmul  22677  ressprdsds  24317  nmpropd  24540  tng0  24589  tngngp2  24598  tnggrpr  24601  tngnrg  24620  sranlm  24630  pi1addval  25006  cvsi  25088  tcphphl  25185  abvpropd2  33026  resv0g  33398  resvcmn  33400  sra1r  33716  sradrng  33717  sraidom  33718  srasubrg  33719  srapwov  33724  drgextlsp  33729  tnglvec  33748  tngdim  33749  matdim  33751  fedgmullem2  33766  fldextrspunfld  33812  zhmnrg  34101  prdsbnd  37963  prdstotbnd  37964  prdsbnd2  37965  erngdvlem3  41285  erngdvlem3-rN  41293  hlhils0  42240  hlhils1N  42241  hlhillvec  42246  hlhildrng  42247  hlhil0  42250  hlhillsm  42251  zndvdchrrhm  42261  isprimroot  42382  primrootsunit1  42386  mendval  43458  mnring0gd  44499  mnringlmodd  44504  ovmpt4d  49147  upfval  49458  prcofvalg  49658