Theorem oveqdr 7437

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

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

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3916  df-uni 4868  df-br 5104  df-iota 6484  df-fv 6536  df-ov 7412

This theorem is used by:  fullresc  17973  fucpropd  18102  resssetc  18214  resscatc  18231  issstrmgm  18778  gsumpropd  18814  issubmgm2  18839  grpsubpropd  19202  sylow2blem2  19782  isrngd  20342  prdsrngd  20345  isringd  20469  prdsringd  20497  prdscrngd  20498  prds1  20499  rnghmval  20617  pwsco1rhm  20688  pwsco2rhm  20689  pwsdiagrhm  20806  rnghmsubcsetclem1  20830  rnghmsubcsetclem2  20831  rngcifuestrc  20838  rhmsubcsetclem1  20859  rhmsubcsetclem2  20860  rhmsubcrngclem1  20865  rhmsubcrngclem2  20866  isdomn  20904  primefld  21009  sraring  21408  sralmod  21409  sralmod0  21410  issubrgd  21411  znzrh  21795  zncrng  21797  phlssphl  21912  opsrcrng  22315  opsrassa  22316  ply1lss  22461  ply1subrg  22462  opsr0  22483  opsr1  22484  subrgply1  22497  opsrring  22509  opsrlmod  22510  ply1mpl0  22521  ply1mpl1  22523  ply1ascl  22524  coe1tm  22539  evls1rhm  22587  evl1rhm  22597  evl1expd  22610  evls1maplmhm  22642  mat0  22679  matinvg  22680  matlmod  22691  scmatsrng1  22785  1mavmul  22810  mat2pmatmul  22996  ressprdsds  24637  nmpropd  24860  tng0  24909  tngngp2  24918  tnggrpr  24921  tngnrg  24940  sranlm  24950  pi1addval  25316  cvsi  25398  tcphphl  25495  abvpropd2  33445  resv0g  33818  resvcmn  33820  sra1r  34132  sradrng  34133  sraidom  34134  srasubrg  34135  srapwov  34140  drgextlsp  34145  tnglvec  34163  tngdim  34164  matdim  34166  fedgmullem2  34181  fldextrspunfld  34227  zhmnrg  34516  prdsbnd  38641  prdstotbnd  38642  prdsbnd2  38643  erngdvlem3  41961  erngdvlem3-rN  41969  hlhils0  42916  hlhils1N  42917  hlhillvec  42922  hlhildrng  42923  hlhil0  42926  hlhillsm  42927  zndvdchrrhm  42937  isprimroot  43057  primrootsunit1  43061  mendval  44118  mnring0gd  45157  mnringlmodd  45162  ovmpt4d  49891  upfval  50200  prcofvalg  50400