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

Theorem proplem3 14946
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 6301 . 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 1379  (class class class)co 6284
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rex 2820  df-uni 4246  df-br 4448  df-iota 5551  df-fv 5596  df-ov 6287
This theorem is referenced by:  fullresc  15078  fucpropd  15204  resssetc  15277  resscatc  15290  gsumpropd  15826  grpsubpropd  15950  sylow2blem2  16447  isrngd  17034  prdsrngd  17062  prdscrngd  17063  prds1  17064  pwsco1rhm  17187  pwsco2rhm  17188  pwsdiagrhm  17262  sralmod  17633  sralmod0  17634  issubrngd2  17635  isdomn  17742  sraassa  17773  opsrcrng  17951  opsrassa  17952  ply1lss  18034  ply1subrg  18035  opsr0  18058  opsr1  18059  subrgply1  18073  opsrrng  18085  opsrlmod  18086  ply1mpl0  18095  ply1mpl1  18097  ply1ascl  18098  coe1tm  18113  evls1rhm  18158  evl1rhm  18167  evl1expd  18180  znzrh  18376  zncrng  18378  mat0  18714  matinvg  18715  matlmod  18726  scmatsrng1  18820  1mavmul  18845  mat2pmatmul  19027  ressprdsds  20637  nmpropd  20877  tng0  20920  tngngp2  20929  tngnrg  20946  sranlm  20956  tchphl  21433  istrkgc  23607  istrkgb  23608  abvpropd2  27330  zhmnrg  27612  prdsbnd  29920  prdstotbnd  29921  prdsbnd2  29922  mendval  30765  erngdvlem3  35804  erngdvlem3-rN  35812  hlhils0  36763  hlhils1N  36764  hlhillvec  36769  hlhildrng  36770  hlhil0  36773  hlhillsm  36774
  Copyright terms: Public domain W3C validator