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

Theorem ralim 2793
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 2792 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 2754
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652
This theorem depends on definitions:  df-bi 185  df-ral 2759
This theorem is referenced by:  ralimdaa  2806  r19.30  2952  trint  4504  mpteqb  5948  tz7.49  7147  mptelixpg  7544  resixpfo  7545  bnd  8342  kmlem12  8573  lbzbi  11215  r19.29uz  13332  caubnd  13340  alzdvds  14245  ptclsg  20408  isucn2  21074  usgreghash2spot  25486  omssubadd  28748  dfon2lem8  30009  dford3lem2  35331
  Copyright terms: Public domain W3C validator