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

Theorem ralim 2853
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 2852 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 2814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612
This theorem depends on definitions:  df-bi 185  df-ral 2819
This theorem is referenced by:  ralimdaa  2866  r19.30  3006  trint  4555  mpteqb  5962  tz7.49  7107  mptelixpg  7503  resixpfo  7504  bnd  8306  kmlem12  8537  lbzbi  11166  r19.29uz  13139  caubnd  13147  alzdvds  13888  ptclsg  19848  isucn2  20514  usgreghash2spot  24743  dfon2lem8  28796  dford3lem2  30573
  Copyright terms: Public domain W3C validator