Theorem oveqdr 6674

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	|- ( ph -> F = G )

Assertion

Ref	Expression
oveqdr	|- ( ( ph /\ ps ) -> ( x F y ) = ( x G y ) )

Proof of Theorem oveqdr

Step	Hyp	Ref	Expression
1		oveqdr.1	. . 3 |- ( ph -> F = G )
2	1	oveqd 6667	. 2 |- ( ph -> ( x F y ) = ( x G y ) )
3	2	adantr 481	1 |- ( ( ph /\ ps ) -> ( x F y ) = ( x G y ) )

Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483  (class class class)co 6650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653

This theorem is referenced by:  fullresc  16511  fucpropd  16637  resssetc  16742  resscatc  16755  issstrmgm  17252  gsumpropd  17272  grpsubpropd  17520  sylow2blem2  18036  isringd  18585  prdsringd  18612  prdscrngd  18613  prds1  18614  pwsco1rhm  18738  pwsco2rhm  18739  pwsdiagrhm  18813  sralmod  19187  sralmod0  19188  issubrngd2  19189  isdomn  19294  sraassa  19325  opsrcrng  19488  opsrassa  19489  ply1lss  19566  ply1subrg  19567  opsr0  19588  opsr1  19589  subrgply1  19603  opsrring  19615  opsrlmod  19616  ply1mpl0  19625  ply1mpl1  19627  ply1ascl  19628  coe1tm  19643  evls1rhm  19687  evl1rhm  19696  evl1expd  19709  znzrh  19891  zncrng  19893  mat0  20223  matinvg  20224  matlmod  20235  scmatsrng1  20329  1mavmul  20354  mat2pmatmul  20536  ressprdsds  22176  nmpropd  22398  tng0  22447  tngngp2  22456  tnggrpr  22459  tngnrg  22478  sranlm  22488  tchphl  23026  istrkgc  25353  istrkgb  25354  abvpropd2  29652  resv0g  29836  resvcmn  29838  zhmnrg  30011  prdsbnd  33592  prdstotbnd  33593  prdsbnd2  33594  erngdvlem3  36278  erngdvlem3-rN  36286  hlhils0  37237  hlhils1N  37238  hlhillvec  37243  hlhildrng  37244  hlhil0  37247  hlhillsm  37248  mendval  37753  issubmgm2  41790  rnghmval  41891  lidlmmgm  41925  rnghmsubcsetclem1  41975  rnghmsubcsetclem2  41976  rngcifuestrc  41997  rhmsubcsetclem1  42021  rhmsubcsetclem2  42022  rhmsubcrngclem1  42027  rhmsubcrngclem2  42028