Theorem oveqdr 6573

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

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475  (class class class)co 6549

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552

This theorem is referenced by:  fullresc  16334  fucpropd  16460  resssetc  16565  resscatc  16578  issstrmgm  17075  gsumpropd  17095  grpsubpropd  17343  sylow2blem2  17859  isringd  18408  prdsringd  18435  prdscrngd  18436  prds1  18437  pwsco1rhm  18561  pwsco2rhm  18562  pwsdiagrhm  18636  sralmod  19008  sralmod0  19009  issubrngd2  19010  isdomn  19115  sraassa  19146  opsrcrng  19309  opsrassa  19310  ply1lss  19387  ply1subrg  19388  opsr0  19409  opsr1  19410  subrgply1  19424  opsrring  19436  opsrlmod  19437  ply1mpl0  19446  ply1mpl1  19448  ply1ascl  19449  coe1tm  19464  evls1rhm  19508  evl1rhm  19517  evl1expd  19530  znzrh  19710  zncrng  19712  mat0  20042  matinvg  20043  matlmod  20054  scmatsrng1  20148  1mavmul  20173  mat2pmatmul  20355  ressprdsds  21986  nmpropd  22208  tng0  22257  tngngp2  22266  tnggrpr  22269  tngnrg  22288  sranlm  22298  tchphl  22834  istrkgc  25153  istrkgb  25154  abvpropd2  28983  resv0g  29167  resvcmn  29169  zhmnrg  29339  prdsbnd  32762  prdstotbnd  32763  prdsbnd2  32764  erngdvlem3  35296  erngdvlem3-rN  35304  hlhils0  36255  hlhils1N  36256  hlhillvec  36261  hlhildrng  36262  hlhil0  36265  hlhillsm  36266  mendval  36772  issubmgm2  41580  rnghmval  41681  lidlmmgm  41715  rnghmsubcsetclem1  41767  rnghmsubcsetclem2  41768  rngcifuestrc  41789  rhmsubcsetclem1  41813  rhmsubcsetclem2  41814  rhmsubcrngclem1  41819  rhmsubcrngclem2  41820