Theorem oveqdr 7283

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539  (class class class)co 7255

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258

This theorem is referenced by:  fullresc  17482  fucpropd  17611  resssetc  17723  resscatc  17740  issstrmgm  18252  gsumpropd  18277  grpsubpropd  18595  sylow2blem2  19141  isringd  19739  prdsringd  19766  prdscrngd  19767  prds1  19768  pwsco1rhm  19897  pwsco2rhm  19898  pwsdiagrhm  19973  primefld  19988  sralmod  20370  sralmod0  20371  issubrngd2  20372  isdomn  20478  znzrh  20662  zncrng  20664  phlssphl  20776  sraassa  20984  opsrcrng  21176  opsrassa  21177  ply1lss  21277  ply1subrg  21278  opsr0  21299  opsr1  21300  subrgply1  21314  opsrring  21326  opsrlmod  21327  ply1mpl0  21336  ply1mpl1  21338  ply1ascl  21339  coe1tm  21354  evls1rhm  21398  evl1rhm  21408  evl1expd  21421  mat0  21474  matinvg  21475  matlmod  21486  scmatsrng1  21580  1mavmul  21605  mat2pmatmul  21788  ressprdsds  23432  nmpropd  23656  tng0  23708  tngngp2  23722  tnggrpr  23725  tngnrg  23744  sranlm  23754  pi1addval  24117  cvsi  24199  tcphphl  24296  istrkgc  26719  istrkgb  26720  abvpropd2  31139  resv0g  31442  resvcmn  31444  sra1r  31573  sraring  31574  sradrng  31575  srasubrg  31576  drgextlsp  31583  tnglvec  31597  tngdim  31598  matdim  31600  fedgmullem2  31613  zhmnrg  31817  prdsbnd  35878  prdstotbnd  35879  prdsbnd2  35880  erngdvlem3  38931  erngdvlem3-rN  38939  hlhils0  39890  hlhils1N  39891  hlhillvec  39896  hlhildrng  39897  hlhil0  39900  hlhillsm  39901  mendval  40924  mnring0gd  41726  mnringlmodd  41733  issubmgm2  45232  rnghmval  45337  lidlmmgm  45371  rnghmsubcsetclem1  45421  rnghmsubcsetclem2  45422  rngcifuestrc  45443  rhmsubcsetclem1  45467  rhmsubcsetclem2  45468  rhmsubcrngclem1  45473  rhmsubcrngclem2  45474