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

Theorem proplem3 14625
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 6107 . 2  |-  ( ph  ->  ( x F y )  =  ( x G y ) )
32adantr 462 1  |-  ( (
ph  /\  ps )  ->  ( x F y )  =  ( x G y ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1364  (class class class)co 6090
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-rex 2719  df-uni 4089  df-br 4290  df-iota 5378  df-fv 5423  df-ov 6093
This theorem is referenced by:  fullresc  14757  fucpropd  14883  resssetc  14956  resscatc  14969  gsumpropd  15499  grpsubpropd  15619  sylow2blem2  16113  isrngd  16669  prdsrngd  16694  prdscrngd  16695  prds1  16696  pwsco1rhm  16810  pwsco2rhm  16811  pwsdiagrhm  16878  sralmod  17246  sralmod0  17247  issubrngd2  17248  isdomn  17344  sraassa  17374  opsrcrng  17557  opsrassa  17558  ply1lss  17607  ply1subrg  17608  opsr0  17627  opsr1  17628  subrgply1  17642  opsrrng  17654  opsrlmod  17655  ply1mpl0  17664  ply1mpl1  17665  ply1ascl  17666  coe1tm  17680  znzrh  17875  zncrng  17877  mat0  18218  matinvg  18219  matlmod  18229  1mavmul  18259  ressprdsds  19846  nmpropd  20086  tng0  20129  tngngp2  20138  tngnrg  20155  sranlm  20165  tchphl  20642  evl1rhm  21438  evl1expd  21447  istrkgc  22860  istrkgb  22861  abvpropd2  26030  zhmnrg  26316  prdsbnd  28601  prdstotbnd  28602  prdsbnd2  28603  mendval  29449  scmatsrng1  30756  erngdvlem3  34322  erngdvlem3-rN  34330  hlhils0  35281  hlhils1N  35282  hlhillvec  35287  hlhildrng  35288  hlhil0  35291  hlhillsm  35292
  Copyright terms: Public domain W3C validator