Theorem ralim 2846

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

Proof of Theorem ralim

Step	Hyp	Ref	Expression
1		id 22	. 2
2	1	ral2imi 2845	1

Syntax hints:  ->wi 4  A.wral 2807

This theorem is referenced by:  ralimdaa  2859  r19.30  3002  trint  4560  mpteqb  5970  tz7.49  7129  mptelixpg  7526  resixpfo  7527  bnd  8331  kmlem12  8562  lbzbi  11199  r19.29uz  13183  caubnd  13191  alzdvds  14036  ptclsg  20116  isucn2  20782  usgreghash2spot  25069  dfon2lem8  29222  dford3lem2  30969

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

This theorem depends on definitions:  df-bi 185  df-ral 2812