Theorem oveqdr 7476

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537  (class class class)co 7448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451

This theorem is referenced by:  fullresc  17915  fucpropd  18047  resssetc  18159  resscatc  18176  issstrmgm  18691  gsumpropd  18716  issubmgm2  18741  grpsubpropd  19085  sylow2blem2  19663  isrngd  20200  prdsrngd  20203  isringd  20314  prdsringd  20344  prdscrngd  20345  prds1  20346  rnghmval  20466  pwsco1rhm  20528  pwsco2rhm  20529  pwsdiagrhm  20635  rnghmsubcsetclem1  20653  rnghmsubcsetclem2  20654  rngcifuestrc  20661  rhmsubcsetclem1  20682  rhmsubcsetclem2  20683  rhmsubcrngclem1  20688  rhmsubcrngclem2  20689  isdomn  20727  primefld  20828  sraring  21216  sralmod  21217  sralmod0  21218  issubrgd  21219  znzrh  21584  zncrng  21586  phlssphl  21700  sraassaOLD  21913  opsrcrng  22106  opsrassa  22107  ply1lss  22219  ply1subrg  22220  opsr0  22241  opsr1  22242  subrgply1  22255  opsrring  22267  opsrlmod  22268  ply1mpl0  22279  ply1mpl1  22281  ply1ascl  22282  coe1tm  22297  evls1rhm  22347  evl1rhm  22357  evl1expd  22370  evls1maplmhm  22402  mat0  22444  matinvg  22445  matlmod  22456  scmatsrng1  22550  1mavmul  22575  mat2pmatmul  22758  ressprdsds  24402  nmpropd  24628  tng0  24680  tngngp2  24694  tnggrpr  24697  tngnrg  24716  sranlm  24726  pi1addval  25100  cvsi  25182  tcphphl  25280  abvpropd2  32932  resv0g  33332  resvcmn  33334  sra1r  33597  sradrng  33598  srasubrg  33599  drgextlsp  33608  tnglvec  33625  tngdim  33626  matdim  33628  fedgmullem2  33643  zhmnrg  33913  prdsbnd  37753  prdstotbnd  37754  prdsbnd2  37755  erngdvlem3  40947  erngdvlem3-rN  40955  hlhils0  41906  hlhils1N  41907  hlhillvec  41912  hlhildrng  41913  hlhil0  41916  hlhillsm  41917  zndvdchrrhm  41927  isprimroot  42050  primrootsunit1  42054  mendval  43140  mnring0gd  44188  mnringlmodd  44195