Theorem oveqdr 7395

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542  (class class class)co 7367

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-ss 3906  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370

This theorem is referenced by:  fullresc  17818  fucpropd  17947  resssetc  18059  resscatc  18076  issstrmgm  18621  gsumpropd  18646  issubmgm2  18671  grpsubpropd  19021  sylow2blem2  19596  isrngd  20154  prdsrngd  20157  isringd  20272  prdsringd  20300  prdscrngd  20301  prds1  20302  rnghmval  20420  pwsco1rhm  20479  pwsco2rhm  20480  pwsdiagrhm  20584  rnghmsubcsetclem1  20608  rnghmsubcsetclem2  20609  rngcifuestrc  20616  rhmsubcsetclem1  20637  rhmsubcsetclem2  20638  rhmsubcrngclem1  20643  rhmsubcrngclem2  20644  isdomn  20682  primefld  20782  sraring  21181  sralmod  21182  sralmod0  21183  issubrgd  21184  znzrh  21522  zncrng  21524  phlssphl  21639  opsrcrng  22037  opsrassa  22038  ply1lss  22160  ply1subrg  22161  opsr0  22182  opsr1  22183  subrgply1  22196  opsrring  22208  opsrlmod  22209  ply1mpl0  22220  ply1mpl1  22222  ply1ascl  22223  coe1tm  22238  evls1rhm  22287  evl1rhm  22297  evl1expd  22310  evls1maplmhm  22342  mat0  22382  matinvg  22383  matlmod  22394  scmatsrng1  22488  1mavmul  22513  mat2pmatmul  22696  ressprdsds  24336  nmpropd  24559  tng0  24608  tngngp2  24617  tnggrpr  24620  tngnrg  24639  sranlm  24649  pi1addval  25015  cvsi  25097  tcphphl  25194  abvpropd2  33025  resv0g  33398  resvcmn  33400  sra1r  33725  sradrng  33726  sraidom  33727  srasubrg  33728  srapwov  33733  drgextlsp  33738  tnglvec  33756  tngdim  33757  matdim  33759  fedgmullem2  33774  fldextrspunfld  33820  zhmnrg  34109  prdsbnd  38114  prdstotbnd  38115  prdsbnd2  38116  erngdvlem3  41436  erngdvlem3-rN  41444  hlhils0  42391  hlhils1N  42392  hlhillvec  42397  hlhildrng  42398  hlhil0  42401  hlhillsm  42402  zndvdchrrhm  42412  isprimroot  42532  primrootsunit1  42536  mendval  43607  mnring0gd  44648  mnringlmodd  44653  ovmpt4d  49340  upfval  49651  prcofvalg  49851