Theorem oveqdr 7398

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

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

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 3444  df-ss 3920  df-uni 4866  df-br 5101  df-iota 6458  df-fv 6510  df-ov 7373

This theorem is referenced by:  fullresc  17789  fucpropd  17918  resssetc  18030  resscatc  18047  issstrmgm  18592  gsumpropd  18617  issubmgm2  18642  grpsubpropd  18992  sylow2blem2  19567  isrngd  20125  prdsrngd  20128  isringd  20243  prdsringd  20273  prdscrngd  20274  prds1  20275  rnghmval  20393  pwsco1rhm  20452  pwsco2rhm  20453  pwsdiagrhm  20557  rnghmsubcsetclem1  20581  rnghmsubcsetclem2  20582  rngcifuestrc  20589  rhmsubcsetclem1  20610  rhmsubcsetclem2  20611  rhmsubcrngclem1  20616  rhmsubcrngclem2  20617  isdomn  20655  primefld  20755  sraring  21155  sralmod  21156  sralmod0  21157  issubrgd  21158  znzrh  21514  zncrng  21516  phlssphl  21631  sraassaOLD  21842  opsrcrng  22031  opsrassa  22032  ply1lss  22154  ply1subrg  22155  opsr0  22176  opsr1  22177  subrgply1  22190  opsrring  22202  opsrlmod  22203  ply1mpl0  22214  ply1mpl1  22216  ply1ascl  22217  coe1tm  22232  evls1rhm  22283  evl1rhm  22293  evl1expd  22306  evls1maplmhm  22338  mat0  22378  matinvg  22379  matlmod  22390  scmatsrng1  22484  1mavmul  22509  mat2pmatmul  22692  ressprdsds  24332  nmpropd  24555  tng0  24604  tngngp2  24613  tnggrpr  24616  tngnrg  24635  sranlm  24645  pi1addval  25021  cvsi  25103  tcphphl  25200  abvpropd2  33064  resv0g  33437  resvcmn  33439  sra1r  33764  sradrng  33765  sraidom  33766  srasubrg  33767  srapwov  33772  drgextlsp  33777  tnglvec  33796  tngdim  33797  matdim  33799  fedgmullem2  33814  fldextrspunfld  33860  zhmnrg  34149  prdsbnd  38073  prdstotbnd  38074  prdsbnd2  38075  erngdvlem3  41395  erngdvlem3-rN  41403  hlhils0  42350  hlhils1N  42351  hlhillvec  42356  hlhildrng  42357  hlhil0  42360  hlhillsm  42361  zndvdchrrhm  42371  isprimroot  42492  primrootsunit1  42496  mendval  43565  mnring0gd  44606  mnringlmodd  44611  ovmpt4d  49253  upfval  49564  prcofvalg  49764