MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  oveqdr Structured version   Unicode version

Theorem oveqdr 6220
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
StepHypRef Expression
1 oveqdr.1 . . 3  |-  ( ph  ->  F  =  G )
21oveqd 6213 . 2  |-  ( ph  ->  ( x F y )  =  ( x G y ) )
32adantr 463 1  |-  ( (
ph  /\  ps )  ->  ( x F y )  =  ( x G y ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    = wceq 1399  (class class class)co 6196
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-rex 2738  df-uni 4164  df-br 4368  df-iota 5460  df-fv 5504  df-ov 6199
This theorem is referenced by:  fullresc  15257  fucpropd  15383  resssetc  15488  resscatc  15501  gsumpropd  16016  grpsubpropd  16257  sylow2blem2  16758  isringd  17346  prdsringd  17374  prdscrngd  17375  prds1  17376  pwsco1rhm  17500  pwsco2rhm  17501  pwsdiagrhm  17575  sralmod  17946  sralmod0  17947  issubrngd2  17948  isdomn  18056  sraassa  18087  opsrcrng  18265  opsrassa  18266  ply1lss  18348  ply1subrg  18349  opsr0  18372  opsr1  18373  subrgply1  18387  opsrring  18399  opsrlmod  18400  ply1mpl0  18409  ply1mpl1  18411  ply1ascl  18412  coe1tm  18427  evls1rhm  18472  evl1rhm  18481  evl1expd  18494  znzrh  18672  zncrng  18674  mat0  19004  matinvg  19005  matlmod  19016  scmatsrng1  19110  1mavmul  19135  mat2pmatmul  19317  ressprdsds  20959  nmpropd  21199  tng0  21242  tngngp2  21251  tngnrg  21268  sranlm  21278  tchphl  21755  istrkgc  23968  istrkgb  23969  abvpropd2  27793  resv0g  27980  resvcmn  27982  zhmnrg  28101  prdsbnd  30455  prdstotbnd  30456  prdsbnd2  30457  mendval  31300  issubmgm2  32796  rnghmval  32897  lidlmmgm  32931  rnghmsubcsetclem1  32983  rnghmsubcsetclem2  32984  rngcifuestrc  33005  rhmsubcsetclem1  33029  rhmsubcsetclem2  33030  rhmsubcrngclem1  33035  rhmsubcrngclem2  33036  erngdvlem3  37129  erngdvlem3-rN  37137  hlhils0  38088  hlhils1N  38089  hlhillvec  38094  hlhildrng  38095  hlhil0  38098  hlhillsm  38099
  Copyright terms: Public domain W3C validator