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 482	1 ⊢ ((𝜑 ∧ 𝜓) → (𝑥𝐹𝑦) = (𝑥𝐺𝑦))

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542  (class class class)co 7409

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412

This theorem is referenced by:  fullresc  17801  fucpropd  17930  resssetc  18042  resscatc  18059  issstrmgm  18572  gsumpropd  18597  grpsubpropd  18928  sylow2blem2  19489  isringd  20105  prdsringd  20134  prdscrngd  20135  prds1  20136  pwsco1rhm  20277  pwsco2rhm  20278  pwsdiagrhm  20354  primefld  20421  sraring  20808  sralmod  20809  sralmod0  20810  issubrgd  20811  isdomn  20910  znzrh  21098  zncrng  21100  phlssphl  21212  sraassaOLD  21424  opsrcrng  21620  opsrassa  21621  ply1lss  21720  ply1subrg  21721  opsr0  21742  opsr1  21743  subrgply1  21755  opsrring  21767  opsrlmod  21768  ply1mpl0  21777  ply1mpl1  21779  ply1ascl  21780  coe1tm  21795  evls1rhm  21841  evl1rhm  21851  evl1expd  21864  mat0  21919  matinvg  21920  matlmod  21931  scmatsrng1  22025  1mavmul  22050  mat2pmatmul  22233  ressprdsds  23877  nmpropd  24103  tng0  24155  tngngp2  24169  tnggrpr  24172  tngnrg  24191  sranlm  24201  pi1addval  24564  cvsi  24646  tcphphl  24744  abvpropd2  32160  resv0g  32486  resvcmn  32488  sra1r  32703  sradrng  32704  srasubrg  32705  drgextlsp  32712  tnglvec  32728  tngdim  32729  matdim  32731  fedgmullem2  32746  evls1maplmhm  32791  zhmnrg  32978  prdsbnd  36709  prdstotbnd  36710  prdsbnd2  36711  erngdvlem3  39909  erngdvlem3-rN  39917  hlhils0  40868  hlhils1N  40869  hlhillvec  40874  hlhildrng  40875  hlhil0  40878  hlhillsm  40879  mendval  41973  mnring0gd  43026  mnringlmodd  43033  issubmgm2  46608  isrngd  46720  prdsrngd  46725  rnghmval  46737  rnghmsubcsetclem1  46921  rnghmsubcsetclem2  46922  rngcifuestrc  46943  rhmsubcsetclem1  46967  rhmsubcsetclem2  46968  rhmsubcrngclem1  46973  rhmsubcrngclem2  46974