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

Theorem proplem3 13843
Description: Lemma for property theorems. (Contributed by Mario Carneiro, 29-Jun-2015.)
Hypothesis
Ref Expression
proplem3.1  |-  ( ph  ->  F  =  G )
Assertion
Ref Expression
proplem3  |-  ( (
ph  /\  ps )  ->  ( x F y )  =  ( x G y ) )

Proof of Theorem proplem3
StepHypRef Expression
1 proplem3.1 . . 3  |-  ( ph  ->  F  =  G )
21oveqd 6037 . 2  |-  ( ph  ->  ( x F y )  =  ( x G y ) )
32adantr 452 1  |-  ( (
ph  /\  ps )  ->  ( x F y )  =  ( x G y ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649  (class class class)co 6020
This theorem is referenced by:  fullresc  13975  fucpropd  14101  resssetc  14174  resscatc  14187  gsumpropd  14703  grpsubpropd  14816  sylow2blem2  15182  isrngd  15625  prdsrngd  15645  prdscrngd  15646  prds1  15647  pwsco1rhm  15760  pwsco2rhm  15761  pwsdiagrhm  15828  sralmod  16185  sralmod0  16186  issubrngd2  16189  isdomn  16281  sraassa  16311  opsrcrng  16475  opsrassa  16476  ply1lss  16521  ply1subrg  16522  opsr0  16539  opsr1  16540  subrgply1  16554  opsrrng  16566  opsrlmod  16567  ply1mpl0  16576  ply1mpl1  16577  ply1ascl  16578  coe1tm  16592  znzrh  16746  zncrng  16748  ressprdsds  18309  nmpropd  18512  tng0  18555  tngngp2  18564  tngnrg  18581  sranlm  18591  tchphl  19056  evl1rhm  19816  evl1expd  19825  abvpropd2  24024  zhmnrg  24152  prdsbnd  26193  prdstotbnd  26194  prdsbnd2  26195  mat0  27141  matinvg  27142  matlmod  27148  mendval  27160  erngdvlem3  31104  erngdvlem3-rN  31112  hlhils0  32063  hlhils1N  32064  hlhillvec  32069  hlhildrng  32070  hlhil0  32073  hlhillsm  32074
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-rex 2655  df-uni 3958  df-br 4154  df-iota 5358  df-fv 5402  df-ov 6023
  Copyright terms: Public domain W3C validator