Theorem oveqdr 7444

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570  (class class class)co 7416

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-ss 3919  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7419

This theorem is used by:  fullresc  17944  fucpropd  18073  resssetc  18185  resscatc  18202  issstrmgm  18749  gsumpropd  18782  issubmgm2  18807  grpsubpropd  19169  sylow2blem2  19749  isrngd  20309  prdsrngd  20312  isringd  20434  prdsringd  20462  prdscrngd  20463  prds1  20464  rnghmval  20582  pwsco1rhm  20653  pwsco2rhm  20654  pwsdiagrhm  20770  rnghmsubcsetclem1  20794  rnghmsubcsetclem2  20795  rngcifuestrc  20802  rhmsubcsetclem1  20823  rhmsubcsetclem2  20824  rhmsubcrngclem1  20829  rhmsubcrngclem2  20830  isdomn  20868  primefld  20972  sraring  21371  sralmod  21372  sralmod0  21373  issubrgd  21374  znzrh  21756  zncrng  21758  phlssphl  21873  opsrcrng  22276  opsrassa  22277  ply1lss  22422  ply1subrg  22423  opsr0  22444  opsr1  22445  subrgply1  22458  opsrring  22470  opsrlmod  22471  ply1mpl0  22482  ply1mpl1  22484  ply1ascl  22485  coe1tm  22500  evls1rhm  22548  evl1rhm  22558  evl1expd  22571  evls1maplmhm  22603  mat0  22640  matinvg  22641  matlmod  22652  scmatsrng1  22746  1mavmul  22771  mat2pmatmul  22957  ressprdsds  24598  nmpropd  24821  tng0  24870  tngngp2  24879  tnggrpr  24882  tngnrg  24901  sranlm  24911  pi1addval  25277  cvsi  25359  tcphphl  25456  abvpropd2  33392  resv0g  33765  resvcmn  33767  sra1r  34078  sradrng  34079  sraidom  34080  srasubrg  34081  srapwov  34086  drgextlsp  34091  tnglvec  34109  tngdim  34110  matdim  34112  fedgmullem2  34127  fldextrspunfld  34173  zhmnrg  34462  prdsbnd  38530  prdstotbnd  38531  prdsbnd2  38532  erngdvlem3  41850  erngdvlem3-rN  41858  hlhils0  42805  hlhils1N  42806  hlhillvec  42811  hlhildrng  42812  hlhil0  42815  hlhillsm  42816  zndvdchrrhm  42826  isprimroot  42946  primrootsunit1  42950  mendval  44007  mnring0gd  45046  mnringlmodd  45051  ovmpt4d  49780  upfval  50089  prcofvalg  50289