Theorem oveqdr 7421

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541  (class class class)co 7393

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3951  df-ss 3961  df-uni 4902  df-br 5142  df-iota 6484  df-fv 6540  df-ov 7396

This theorem is referenced by:  fullresc  17783  fucpropd  17912  resssetc  18024  resscatc  18041  issstrmgm  18554  gsumpropd  18579  grpsubpropd  18902  sylow2blem2  19453  isringd  20062  prdsringd  20089  prdscrngd  20090  prds1  20091  pwsco1rhm  20227  pwsco2rhm  20228  pwsdiagrhm  20348  primefld  20370  sralmod  20757  sralmod0  20758  issubrngd2  20759  isdomn  20846  znzrh  21031  zncrng  21033  phlssphl  21145  sraassa  21355  opsrcrng  21548  opsrassa  21549  ply1lss  21649  ply1subrg  21650  opsr0  21671  opsr1  21672  subrgply1  21686  opsrring  21698  opsrlmod  21699  ply1mpl0  21708  ply1mpl1  21710  ply1ascl  21711  coe1tm  21726  evls1rhm  21770  evl1rhm  21780  evl1expd  21793  mat0  21848  matinvg  21849  matlmod  21860  scmatsrng1  21954  1mavmul  21979  mat2pmatmul  22162  ressprdsds  23806  nmpropd  24032  tng0  24084  tngngp2  24098  tnggrpr  24101  tngnrg  24120  sranlm  24130  pi1addval  24493  cvsi  24575  tcphphl  24673  abvpropd2  32000  resv0g  32317  resvcmn  32319  sra1r  32508  sraring  32509  sradrng  32510  srasubrg  32511  drgextlsp  32518  tnglvec  32533  tngdim  32534  matdim  32536  fedgmullem2  32551  evls1maplmhm  32595  zhmnrg  32776  prdsbnd  36464  prdstotbnd  36465  prdsbnd2  36466  erngdvlem3  39664  erngdvlem3-rN  39672  hlhils0  40623  hlhils1N  40624  hlhillvec  40629  hlhildrng  40630  hlhil0  40633  hlhillsm  40634  mendval  41694  mnring0gd  42747  mnringlmodd  42754  issubmgm2  46330  rnghmval  46435  lidlmmgm  46469  rnghmsubcsetclem1  46519  rnghmsubcsetclem2  46520  rngcifuestrc  46541  rhmsubcsetclem1  46565  rhmsubcsetclem2  46566  rhmsubcrngclem1  46571  rhmsubcrngclem2  46572