Theorem oveqdr 6829

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

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1624  (class class class)co 6805

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-rex 3048  df-uni 4581  df-br 4797  df-iota 6004  df-fv 6049  df-ov 6808

This theorem is referenced by:  fullresc  16704  fucpropd  16830  resssetc  16935  resscatc  16948  issstrmgm  17445  gsumpropd  17465  grpsubpropd  17713  sylow2blem2  18228  isringd  18777  prdsringd  18804  prdscrngd  18805  prds1  18806  pwsco1rhm  18932  pwsco2rhm  18933  pwsdiagrhm  19007  sralmod  19381  sralmod0  19382  issubrngd2  19383  isdomn  19488  sraassa  19519  opsrcrng  19682  opsrassa  19683  ply1lss  19760  ply1subrg  19761  opsr0  19782  opsr1  19783  subrgply1  19797  opsrring  19809  opsrlmod  19810  ply1mpl0  19819  ply1mpl1  19821  ply1ascl  19822  coe1tm  19837  evls1rhm  19881  evl1rhm  19890  evl1expd  19903  znzrh  20085  zncrng  20087  mat0  20417  matinvg  20418  matlmod  20429  scmatsrng1  20523  1mavmul  20548  mat2pmatmul  20730  ressprdsds  22369  nmpropd  22591  tng0  22640  tngngp2  22649  tnggrpr  22652  tngnrg  22671  sranlm  22681  tchphl  23218  istrkgc  25544  istrkgb  25545  abvpropd2  29953  resv0g  30137  resvcmn  30139  zhmnrg  30312  prdsbnd  33897  prdstotbnd  33898  prdsbnd2  33899  erngdvlem3  36772  erngdvlem3-rN  36780  hlhils0  37731  hlhils1N  37732  hlhillvec  37737  hlhildrng  37738  hlhil0  37741  hlhillsm  37742  mendval  38247  issubmgm2  42292  rnghmval  42393  lidlmmgm  42427  rnghmsubcsetclem1  42477  rnghmsubcsetclem2  42478  rngcifuestrc  42499  rhmsubcsetclem1  42523  rhmsubcsetclem2  42524  rhmsubcrngclem1  42529  rhmsubcrngclem2  42530