Theorem oveqdr 7426

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1562  (class class class)co 7398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-v 3458  df-ss 3923  df-uni 4868  df-br 5103  df-iota 6479  df-fv 6531  df-ov 7401

This theorem is referenced by:  fullresc  17886  fucpropd  18015  resssetc  18127  resscatc  18144  issstrmgm  18689  gsumpropd  18714  issubmgm2  18739  grpsubpropd  19089  sylow2blem2  19663  isrngd  20221  prdsrngd  20224  isringd  20343  prdsringd  20371  prdscrngd  20372  prds1  20373  rnghmval  20491  pwsco1rhm  20553  pwsco2rhm  20554  pwsdiagrhm  20659  rnghmsubcsetclem1  20683  rnghmsubcsetclem2  20684  rngcifuestrc  20691  rhmsubcsetclem1  20712  rhmsubcsetclem2  20713  rhmsubcrngclem1  20718  rhmsubcrngclem2  20719  isdomn  20757  primefld  20856  sraring  21255  sralmod  21256  sralmod0  21257  issubrgd  21258  znzrh  21596  zncrng  21598  phlssphl  21713  opsrcrng  22114  opsrassa  22115  ply1lss  22260  ply1subrg  22261  opsr0  22282  opsr1  22283  subrgply1  22296  opsrring  22308  opsrlmod  22309  ply1mpl0  22320  ply1mpl1  22322  ply1ascl  22323  coe1tm  22338  evls1rhm  22387  evl1rhm  22397  evl1expd  22410  evls1maplmhm  22442  mat0  22479  matinvg  22480  matlmod  22491  scmatsrng1  22585  1mavmul  22610  mat2pmatmul  22793  ressprdsds  24433  nmpropd  24656  tng0  24705  tngngp2  24714  tnggrpr  24717  tngnrg  24736  sranlm  24746  pi1addval  25112  cvsi  25194  tcphphl  25291  abvpropd2  33145  resv0g  33526  resvcmn  33528  sra1r  33880  sradrng  33881  sraidom  33882  srasubrg  33883  srapwov  33888  drgextlsp  33893  tnglvec  33911  tngdim  33912  matdim  33914  fedgmullem2  33929  fldextrspunfld  33975  zhmnrg  34264  prdsbnd  38297  prdstotbnd  38298  prdsbnd2  38299  erngdvlem3  41619  erngdvlem3-rN  41627  hlhils0  42574  hlhils1N  42575  hlhillvec  42580  hlhildrng  42581  hlhil0  42584  hlhillsm  42585  zndvdchrrhm  42595  isprimroot  42715  primrootsunit1  42719  mendval  43761  mnring0gd  44802  mnringlmodd  44807  ovmpt4d  49491  upfval  49802  prcofvalg  50002