Theorem ralim 3085

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 3084	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓))

Syntax hints:   → wi 4  ∀wral 3060

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

This theorem depends on definitions:  df-bi 206  df-ral 3061

This theorem is referenced by:  r19.30OLD  3120  ralimdaa  3241  mpteqb  6972  tz7.49  8396  mptelixpg  8880  resixpfo  8881  bnd  9837  kmlem12  10106  lbzbi  12870  r19.29uz  15247  caubnd  15255  alzdvds  16213  ptclsg  23003  isucn2  23668  fusgreghash2wsp  29345  omssubadd  32989  subgrwlk  33813  dfon2lem8  34451  fvineqsneq  35956  dford3lem2  41409  neik0pk1imk0  42441  grur1cld  42634  mnuprdlem4  42677  mnurndlem1  42683