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

Theorem proplem3 13593
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 5875 . 2  |-  ( ph  ->  ( x F y )  =  ( x G y ) )
32adantr 451 1  |-  ( (
ph  /\  ps )  ->  ( x F y )  =  ( x G y ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1623  (class class class)co 5858
This theorem is referenced by:  resssetc  13924  resscatc  13937  gsumpropd  14453  grpsubpropd  14566  prdsrngd  15395  prdscrngd  15396  prds1  15397  pwsco1rhm  15510  pwsco2rhm  15511  pwsdiagrhm  15578  sralmod  15939  sralmod0  15940  issubrngd2  15943  sraassa  16065  opsrcrng  16229  opsrassa  16230  ply1lss  16275  ply1subrg  16276  opsr0  16295  opsr1  16296  subrgply1  16311  opsrrng  16323  opsrlmod  16324  ply1mpl0  16333  ply1mpl1  16334  ply1ascl  16335  coe1tm  16349  znzrh  16496  zncrng  16498  ressprdsds  17935  nmpropd  18116  tng0  18159  tngngp2  18168  tngnrg  18185  sranlm  18195  tchphl  18658  evl1rhm  19412  evl1expd  19421  prdsbnd  26517  prdstotbnd  26518  prdsbnd2  26519  mat0  27472  matinvg  27473  matlmod  27479  hlhils0  32138  hlhils1N  32139  hlhillvec  32144  hlhildrng  32145  hlhil0  32148  hlhillsm  32149
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-ov 5861
  Copyright terms: Public domain W3C validator