Theorem oveqdr 7439

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567  (class class class)co 7411

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3463  df-ss 3928  df-uni 4875  df-br 5112  df-iota 6493  df-fv 6545  df-ov 7414

This theorem is referenced by:  fullresc  17908  fucpropd  18037  resssetc  18149  resscatc  18166  issstrmgm  18711  gsumpropd  18736  issubmgm2  18761  grpsubpropd  19111  sylow2blem2  19691  isrngd  20251  prdsrngd  20254  isringd  20374  prdsringd  20402  prdscrngd  20403  prds1  20404  rnghmval  20522  pwsco1rhm  20584  pwsco2rhm  20585  pwsdiagrhm  20692  rnghmsubcsetclem1  20716  rnghmsubcsetclem2  20717  rngcifuestrc  20724  rhmsubcsetclem1  20745  rhmsubcsetclem2  20746  rhmsubcrngclem1  20751  rhmsubcrngclem2  20752  isdomn  20790  primefld  20886  sraring  21285  sralmod  21286  sralmod0  21287  issubrgd  21288  znzrh  21661  zncrng  21663  phlssphl  21778  opsrcrng  22179  opsrassa  22180  ply1lss  22325  ply1subrg  22326  opsr0  22347  opsr1  22348  subrgply1  22361  opsrring  22373  opsrlmod  22374  ply1mpl0  22385  ply1mpl1  22387  ply1ascl  22388  coe1tm  22403  evls1rhm  22451  evl1rhm  22461  evl1expd  22474  evls1maplmhm  22506  mat0  22543  matinvg  22544  matlmod  22555  scmatsrng1  22649  1mavmul  22674  mat2pmatmul  22857  ressprdsds  24497  nmpropd  24720  tng0  24769  tngngp2  24778  tnggrpr  24781  tngnrg  24800  sranlm  24810  pi1addval  25176  cvsi  25258  tcphphl  25355  abvpropd2  33226  resv0g  33601  resvcmn  33603  sra1r  33916  sradrng  33917  sraidom  33918  srasubrg  33919  srapwov  33924  drgextlsp  33929  tnglvec  33947  tngdim  33948  matdim  33950  fedgmullem2  33965  fldextrspunfld  34011  zhmnrg  34300  prdsbnd  38367  prdstotbnd  38368  prdsbnd2  38369  erngdvlem3  41689  erngdvlem3-rN  41697  hlhils0  42644  hlhils1N  42645  hlhillvec  42650  hlhildrng  42651  hlhil0  42654  hlhillsm  42655  zndvdchrrhm  42665  isprimroot  42785  primrootsunit1  42789  mendval  43833  mnring0gd  44872  mnringlmodd  44877  ovmpt4d  49563  upfval  49874  prcofvalg  50074