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 23 . 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 2775
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678
This theorem depends on definitions:  df-bi 188  df-ral 2780
This theorem is referenced by:  ralimdaa  2827  r19.30  2973  trint  4530  mpteqb  5977  tz7.49  7167  mptelixpg  7564  resixpfo  7565  bnd  8365  kmlem12  8592  lbzbi  11253  r19.29uz  13402  caubnd  13410  alzdvds  14343  ptclsg  20617  isucn2  21281  usgreghash2spot  25783  omssubadd  29124  omssubaddOLD  29128  dfon2lem8  30431  dford3lem2  35802
  Copyright terms: Public domain W3C validator