Theorem ralim 2948

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

Step	Hyp	Ref	Expression
1		id 22	. 2 |- ( ( ph -> ps ) -> ( ph -> ps ) )
2	1	ral2imi 2947	1 |- ( A. x e. A ( ph -> ps ) -> ( A. x e. A ph -> A. x e. A ps ) )

Syntax hints:   -> wi 4   A.wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737

This theorem depends on definitions:  df-bi 197  df-ral 2917

This theorem is referenced by:  ralimdaa  2958  r19.30  3082  trint  4768  mpteqb  6299  tz7.49  7540  mptelixpg  7945  resixpfo  7946  bnd  8755  kmlem12  8983  lbzbi  11776  r19.29uz  14090  caubnd  14098  alzdvds  15042  ptclsg  21418  isucn2  22083  fusgreghash2wsp  27202  omssubadd  30362  dfon2lem8  31695  dford3lem2  37594  neik0pk1imk0  38345