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  32129  resv0g  32455  resvcmn  32457  sra1r  32672  sradrng  32673  srasubrg  32674  drgextlsp  32681  tnglvec  32697  tngdim  32698  matdim  32700  fedgmullem2  32715  evls1maplmhm  32760  zhmnrg  32947  prdsbnd  36661  prdstotbnd  36662  prdsbnd2  36663  erngdvlem3  39861  erngdvlem3-rN  39869  hlhils0  40820  hlhils1N  40821  hlhillvec  40826  hlhildrng  40827  hlhil0  40830  hlhillsm  40831  mendval  41925  mnring0gd  42978  mnringlmodd  42985  issubmgm2  46560  isrngd  46672  prdsrngd  46677  rnghmval  46689  rnghmsubcsetclem1  46873  rnghmsubcsetclem2  46874  rngcifuestrc  46895  rhmsubcsetclem1  46919  rhmsubcsetclem2  46920  rhmsubcrngclem1  46925  rhmsubcrngclem2  46926