Theorem ralim 3077

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

Syntax hints:   → wi 4  ∀wral 3052

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

This theorem depends on definitions:  df-bi 207  df-ral 3053

This theorem is referenced by:  ralimdaa  3247  mpteqb  7010  tz7.49  8464  mptelixpg  8954  resixpfo  8955  bnd  9911  kmlem12  10181  lbzbi  12957  r19.29uz  15374  caubnd  15382  alzdvds  16344  ptclsg  23558  isucn2  24222  fusgreghash2wsp  30324  omssubadd  34337  subgrwlk  35159  dfon2lem8  35813  fvineqsneq  37435  dford3lem2  43018  neik0pk1imk0  44038  grur1cld  44223  mnuprdlem4  44266  mnurndlem1  44272