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

Theorem proplem3 14629
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 6108 . 2  |-  ( ph  ->  ( x F y )  =  ( x G y ) )
32adantr 465 1  |-  ( (
ph  /\  ps )  ->  ( x F y )  =  ( x G y ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1369  (class class class)co 6091
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-rex 2721  df-uni 4092  df-br 4293  df-iota 5381  df-fv 5426  df-ov 6094
This theorem is referenced by:  fullresc  14761  fucpropd  14887  resssetc  14960  resscatc  14973  gsumpropd  15504  grpsubpropd  15626  sylow2blem2  16120  isrngd  16679  prdsrngd  16704  prdscrngd  16705  prds1  16706  pwsco1rhm  16826  pwsco2rhm  16827  pwsdiagrhm  16898  sralmod  17268  sralmod0  17269  issubrngd2  17270  isdomn  17366  sraassa  17396  opsrcrng  17569  opsrassa  17570  ply1lss  17652  ply1subrg  17653  opsr0  17672  opsr1  17673  subrgply1  17687  opsrrng  17700  opsrlmod  17701  ply1mpl0  17710  ply1mpl1  17711  ply1ascl  17712  coe1tm  17726  evls1rhm  17757  evl1rhm  17766  evl1expd  17779  znzrh  17975  zncrng  17977  mat0  18318  matinvg  18319  matlmod  18329  1mavmul  18359  ressprdsds  19946  nmpropd  20186  tng0  20229  tngngp2  20238  tngnrg  20255  sranlm  20265  tchphl  20742  istrkgc  22917  istrkgb  22918  abvpropd2  26113  zhmnrg  26396  prdsbnd  28692  prdstotbnd  28693  prdsbnd2  28694  mendval  29540  scmatsrng1  30890  erngdvlem3  34634  erngdvlem3-rN  34642  hlhils0  35593  hlhils1N  35594  hlhillvec  35599  hlhildrng  35600  hlhil0  35603  hlhillsm  35604
  Copyright terms: Public domain W3C validator