Theorem oveqdr 7303

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539  (class class class)co 7275

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-uni 4840  df-br 5075  df-iota 6391  df-fv 6441  df-ov 7278

This theorem is referenced by:  fullresc  17566  fucpropd  17695  resssetc  17807  resscatc  17824  issstrmgm  18337  gsumpropd  18362  grpsubpropd  18680  sylow2blem2  19226  isringd  19824  prdsringd  19851  prdscrngd  19852  prds1  19853  pwsco1rhm  19982  pwsco2rhm  19983  pwsdiagrhm  20058  primefld  20073  sralmod  20457  sralmod0  20458  issubrngd2  20459  isdomn  20565  znzrh  20750  zncrng  20752  phlssphl  20864  sraassa  21074  opsrcrng  21266  opsrassa  21267  ply1lss  21367  ply1subrg  21368  opsr0  21389  opsr1  21390  subrgply1  21404  opsrring  21416  opsrlmod  21417  ply1mpl0  21426  ply1mpl1  21428  ply1ascl  21429  coe1tm  21444  evls1rhm  21488  evl1rhm  21498  evl1expd  21511  mat0  21566  matinvg  21567  matlmod  21578  scmatsrng1  21672  1mavmul  21697  mat2pmatmul  21880  ressprdsds  23524  nmpropd  23750  tng0  23802  tngngp2  23816  tnggrpr  23819  tngnrg  23838  sranlm  23848  pi1addval  24211  cvsi  24293  tcphphl  24391  istrkgc  26815  istrkgb  26816  abvpropd2  31237  resv0g  31540  resvcmn  31542  sra1r  31671  sraring  31672  sradrng  31673  srasubrg  31674  drgextlsp  31681  tnglvec  31695  tngdim  31696  matdim  31698  fedgmullem2  31711  zhmnrg  31917  prdsbnd  35951  prdstotbnd  35952  prdsbnd2  35953  erngdvlem3  39004  erngdvlem3-rN  39012  hlhils0  39963  hlhils1N  39964  hlhillvec  39969  hlhildrng  39970  hlhil0  39973  hlhillsm  39974  mendval  41008  mnring0gd  41837  mnringlmodd  41844  issubmgm2  45344  rnghmval  45449  lidlmmgm  45483  rnghmsubcsetclem1  45533  rnghmsubcsetclem2  45534  rngcifuestrc  45555  rhmsubcsetclem1  45579  rhmsubcsetclem2  45580  rhmsubcrngclem1  45585  rhmsubcrngclem2  45586