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

Theorem proplem3 13909
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 6091 . 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 1652  (class class class)co 6074
This theorem is referenced by:  fullresc  14041  fucpropd  14167  resssetc  14240  resscatc  14253  gsumpropd  14769  grpsubpropd  14882  sylow2blem2  15248  isrngd  15691  prdsrngd  15711  prdscrngd  15712  prds1  15713  pwsco1rhm  15826  pwsco2rhm  15827  pwsdiagrhm  15894  sralmod  16251  sralmod0  16252  issubrngd2  16255  isdomn  16347  sraassa  16377  opsrcrng  16541  opsrassa  16542  ply1lss  16587  ply1subrg  16588  opsr0  16605  opsr1  16606  subrgply1  16620  opsrrng  16632  opsrlmod  16633  ply1mpl0  16642  ply1mpl1  16643  ply1ascl  16644  coe1tm  16658  znzrh  16816  zncrng  16818  ressprdsds  18394  nmpropd  18634  tng0  18677  tngngp2  18686  tngnrg  18703  sranlm  18713  tchphl  19178  evl1rhm  19942  evl1expd  19951  abvpropd2  24178  zhmnrg  24344  prdsbnd  26494  prdstotbnd  26495  prdsbnd2  26496  mat0  27441  matinvg  27442  matlmod  27448  mendval  27460  erngdvlem3  31725  erngdvlem3-rN  31733  hlhils0  32684  hlhils1N  32685  hlhillvec  32690  hlhildrng  32691  hlhil0  32694  hlhillsm  32695
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rex 2704  df-uni 4009  df-br 4206  df-iota 5411  df-fv 5455  df-ov 6077
  Copyright terms: Public domain W3C validator