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

Theorem ralim 2814
Description: Distribution of restricted quantification over implication. (Contributed by NM, 9-Feb-1997.) (Proof shortened by Wolf Lammen, 1-Dec-2019.)
Assertion
Ref Expression
ralim  |-  ( A. x  e.  A  ( ph  ->  ps )  -> 
( A. x  e.  A  ph  ->  A. x  e.  A  ps )
)

Proof of Theorem ralim
StepHypRef Expression
1 id 22 . 2  |-  ( (
ph  ->  ps )  -> 
( ph  ->  ps )
)
21ral2imi 2813 1  |-  ( A. x  e.  A  ( ph  ->  ps )  -> 
( A. x  e.  A  ph  ->  A. x  e.  A  ps )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wral 2798
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603
This theorem depends on definitions:  df-bi 185  df-ral 2803
This theorem is referenced by:  hbralimdaa  2824  r19.30  2969  trint  4507  mpteqb  5896  tz7.49  7009  mptelixpg  7409  resixpfo  7410  bnd  8209  kmlem12  8440  lbzbi  11053  r19.29uz  12955  caubnd  12963  alzdvds  13700  ptclsg  19319  isucn2  19985  dfon2lem8  27746  dford3lem2  29523  usgreghash2spot  30809
  Copyright terms: Public domain W3C validator