Theorem oveqdr 7163

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538  (class class class)co 7135

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138

This theorem is referenced by:  fullresc  17113  fucpropd  17239  resssetc  17344  resscatc  17357  issstrmgm  17855  gsumpropd  17880  grpsubpropd  18196  sylow2blem2  18738  isringd  19331  prdsringd  19358  prdscrngd  19359  prds1  19360  pwsco1rhm  19486  pwsco2rhm  19487  pwsdiagrhm  19562  primefld  19577  sralmod  19952  sralmod0  19953  issubrngd2  19954  isdomn  20060  znzrh  20234  zncrng  20236  phlssphl  20348  sraassa  20556  opsrcrng  20727  opsrassa  20728  ply1lss  20825  ply1subrg  20826  opsr0  20847  opsr1  20848  subrgply1  20862  opsrring  20874  opsrlmod  20875  ply1mpl0  20884  ply1mpl1  20886  ply1ascl  20887  coe1tm  20902  evls1rhm  20946  evl1rhm  20956  evl1expd  20969  mat0  21022  matinvg  21023  matlmod  21034  scmatsrng1  21128  1mavmul  21153  mat2pmatmul  21336  ressprdsds  22978  nmpropd  23200  tng0  23249  tngngp2  23258  tnggrpr  23261  tngnrg  23280  sranlm  23290  pi1addval  23653  cvsi  23735  tcphphl  23831  istrkgc  26248  istrkgb  26249  abvpropd2  30665  resv0g  30960  resvcmn  30962  sra1r  31074  sraring  31075  sradrng  31076  srasubrg  31077  drgextlsp  31084  tnglvec  31098  tngdim  31099  matdim  31101  fedgmullem2  31114  zhmnrg  31318  prdsbnd  35231  prdstotbnd  35232  prdsbnd2  35233  erngdvlem3  38286  erngdvlem3-rN  38294  hlhils0  39241  hlhils1N  39242  hlhillvec  39247  hlhildrng  39248  hlhil0  39251  hlhillsm  39252  mendval  40127  mnring0gd  40929  mnringlmodd  40934  issubmgm2  44410  rnghmval  44515  lidlmmgm  44549  rnghmsubcsetclem1  44599  rnghmsubcsetclem2  44600  rngcifuestrc  44621  rhmsubcsetclem1  44645  rhmsubcsetclem2  44646  rhmsubcrngclem1  44651  rhmsubcrngclem2  44652