Theorem ralim 3069

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

Syntax hints:   → wi 4  ∀wral 3044

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 3045

This theorem is referenced by:  ralimdaa  3236  mpteqb  6969  tz7.49  8390  mptelixpg  8885  resixpfo  8886  bnd  9821  kmlem12  10091  lbzbi  12871  r19.29uz  15293  caubnd  15301  alzdvds  16266  ptclsg  23478  isucn2  24142  fusgreghash2wsp  30240  omssubadd  34264  subgrwlk  35092  dfon2lem8  35751  fvineqsneq  37373  dford3lem2  42989  neik0pk1imk0  44009  grur1cld  44194  mnuprdlem4  44237  mnurndlem1  44243