Theorem ralim 3130

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

Syntax hints:   → wi 4  ∀wral 3106

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 210  df-ral 3111

This theorem is referenced by:  ralimdaa  3181  r19.30  3293  mpteqb  6764  tz7.49  8064  mptelixpg  8482  resixpfo  8483  bnd  9305  kmlem12  9572  lbzbi  12324  r19.29uz  14702  caubnd  14710  alzdvds  15662  ptclsg  22220  isucn2  22885  fusgreghash2wsp  28123  omssubadd  31668  subgrwlk  32492  dfon2lem8  33148  fvineqsneq  34829  dford3lem2  39968  neik0pk1imk0  40750  grur1cld  40940  mnuprdlem4  40983  mnurndlem1  40989