Theorem oveqdr 7415

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  (class class class)co 7387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-ss 3931  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390

This theorem is referenced by:  fullresc  17813  fucpropd  17942  resssetc  18054  resscatc  18071  issstrmgm  18580  gsumpropd  18605  issubmgm2  18630  grpsubpropd  18977  sylow2blem2  19551  isrngd  20082  prdsrngd  20085  isringd  20200  prdsringd  20230  prdscrngd  20231  prds1  20232  rnghmval  20349  pwsco1rhm  20411  pwsco2rhm  20412  pwsdiagrhm  20516  rnghmsubcsetclem1  20540  rnghmsubcsetclem2  20541  rngcifuestrc  20548  rhmsubcsetclem1  20569  rhmsubcsetclem2  20570  rhmsubcrngclem1  20575  rhmsubcrngclem2  20576  isdomn  20614  primefld  20714  sraring  21093  sralmod  21094  sralmod0  21095  issubrgd  21096  znzrh  21452  zncrng  21454  phlssphl  21568  sraassaOLD  21779  opsrcrng  21966  opsrassa  21967  ply1lss  22081  ply1subrg  22082  opsr0  22103  opsr1  22104  subrgply1  22117  opsrring  22129  opsrlmod  22130  ply1mpl0  22141  ply1mpl1  22143  ply1ascl  22144  coe1tm  22159  evls1rhm  22209  evl1rhm  22219  evl1expd  22232  evls1maplmhm  22264  mat0  22304  matinvg  22305  matlmod  22316  scmatsrng1  22410  1mavmul  22435  mat2pmatmul  22618  ressprdsds  24259  nmpropd  24482  tng0  24531  tngngp2  24540  tnggrpr  24543  tngnrg  24562  sranlm  24572  pi1addval  24948  cvsi  25030  tcphphl  25127  abvpropd2  32887  resv0g  33310  resvcmn  33312  sra1r  33577  sradrng  33578  sraidom  33579  srasubrg  33580  drgextlsp  33589  tnglvec  33608  tngdim  33609  matdim  33611  fedgmullem2  33626  fldextrspunfld  33671  zhmnrg  33955  prdsbnd  37787  prdstotbnd  37788  prdsbnd2  37789  erngdvlem3  40984  erngdvlem3-rN  40992  hlhils0  41939  hlhils1N  41940  hlhillvec  41945  hlhildrng  41946  hlhil0  41949  hlhillsm  41950  zndvdchrrhm  41960  isprimroot  42081  primrootsunit1  42085  mendval  43168  mnring0gd  44210  mnringlmodd  44215  ovmpt4d  48853  upfval  49165  prcofvalg  49365