Theorem oveqdr 7374

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541  (class class class)co 7346

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3914  df-uni 4857  df-br 5090  df-iota 6437  df-fv 6489  df-ov 7349

This theorem is referenced by:  fullresc  17758  fucpropd  17887  resssetc  17999  resscatc  18016  issstrmgm  18561  gsumpropd  18586  issubmgm2  18611  grpsubpropd  18958  sylow2blem2  19533  isrngd  20091  prdsrngd  20094  isringd  20209  prdsringd  20239  prdscrngd  20240  prds1  20241  rnghmval  20358  pwsco1rhm  20417  pwsco2rhm  20418  pwsdiagrhm  20522  rnghmsubcsetclem1  20546  rnghmsubcsetclem2  20547  rngcifuestrc  20554  rhmsubcsetclem1  20575  rhmsubcsetclem2  20576  rhmsubcrngclem1  20581  rhmsubcrngclem2  20582  isdomn  20620  primefld  20720  sraring  21120  sralmod  21121  sralmod0  21122  issubrgd  21123  znzrh  21479  zncrng  21481  phlssphl  21596  sraassaOLD  21807  opsrcrng  21994  opsrassa  21995  ply1lss  22109  ply1subrg  22110  opsr0  22131  opsr1  22132  subrgply1  22145  opsrring  22157  opsrlmod  22158  ply1mpl0  22169  ply1mpl1  22171  ply1ascl  22172  coe1tm  22187  evls1rhm  22237  evl1rhm  22247  evl1expd  22260  evls1maplmhm  22292  mat0  22332  matinvg  22333  matlmod  22344  scmatsrng1  22438  1mavmul  22463  mat2pmatmul  22646  ressprdsds  24286  nmpropd  24509  tng0  24558  tngngp2  24567  tnggrpr  24570  tngnrg  24589  sranlm  24599  pi1addval  24975  cvsi  25057  tcphphl  25154  abvpropd2  32946  resv0g  33303  resvcmn  33305  sra1r  33593  sradrng  33594  sraidom  33595  srasubrg  33596  srapwov  33601  drgextlsp  33606  tnglvec  33625  tngdim  33626  matdim  33628  fedgmullem2  33643  fldextrspunfld  33689  zhmnrg  33978  prdsbnd  37832  prdstotbnd  37833  prdsbnd2  37834  erngdvlem3  41088  erngdvlem3-rN  41096  hlhils0  42043  hlhils1N  42044  hlhillvec  42049  hlhildrng  42050  hlhil0  42053  hlhillsm  42054  zndvdchrrhm  42064  isprimroot  42185  primrootsunit1  42189  mendval  43271  mnring0gd  44313  mnringlmodd  44318  ovmpt4d  48964  upfval  49276  prcofvalg  49476