Theorem oveqdr 7431

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-ss 3943  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538  df-ov 7406

This theorem is referenced by:  fullresc  17862  fucpropd  17991  resssetc  18103  resscatc  18120  issstrmgm  18629  gsumpropd  18654  issubmgm2  18679  grpsubpropd  19026  sylow2blem2  19600  isrngd  20131  prdsrngd  20134  isringd  20249  prdsringd  20279  prdscrngd  20280  prds1  20281  rnghmval  20398  pwsco1rhm  20460  pwsco2rhm  20461  pwsdiagrhm  20565  rnghmsubcsetclem1  20589  rnghmsubcsetclem2  20590  rngcifuestrc  20597  rhmsubcsetclem1  20618  rhmsubcsetclem2  20619  rhmsubcrngclem1  20624  rhmsubcrngclem2  20625  isdomn  20663  primefld  20763  sraring  21142  sralmod  21143  sralmod0  21144  issubrgd  21145  znzrh  21501  zncrng  21503  phlssphl  21617  sraassaOLD  21828  opsrcrng  22015  opsrassa  22016  ply1lss  22130  ply1subrg  22131  opsr0  22152  opsr1  22153  subrgply1  22166  opsrring  22178  opsrlmod  22179  ply1mpl0  22190  ply1mpl1  22192  ply1ascl  22193  coe1tm  22208  evls1rhm  22258  evl1rhm  22268  evl1expd  22281  evls1maplmhm  22313  mat0  22353  matinvg  22354  matlmod  22365  scmatsrng1  22459  1mavmul  22484  mat2pmatmul  22667  ressprdsds  24308  nmpropd  24531  tng0  24580  tngngp2  24589  tnggrpr  24592  tngnrg  24611  sranlm  24621  pi1addval  24997  cvsi  25079  tcphphl  25177  abvpropd2  32887  resv0g  33300  resvcmn  33302  sra1r  33567  sradrng  33568  sraidom  33569  srasubrg  33570  drgextlsp  33579  tnglvec  33598  tngdim  33599  matdim  33601  fedgmullem2  33616  fldextrspunfld  33663  zhmnrg  33942  prdsbnd  37763  prdstotbnd  37764  prdsbnd2  37765  erngdvlem3  40955  erngdvlem3-rN  40963  hlhils0  41910  hlhils1N  41911  hlhillvec  41916  hlhildrng  41917  hlhil0  41920  hlhillsm  41921  zndvdchrrhm  41931  isprimroot  42052  primrootsunit1  42056  mendval  43150  mnring0gd  44193  mnringlmodd  44198  ovmpt4d  48789  upfval  49059  prcofvalg  49235