Theorem ralim 3083

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

Syntax hints:   → wi 4  ∀wral 3064

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

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

This theorem is referenced by:  ralimdaa  3142  r19.30OLD  3269  mpteqb  6894  tz7.49  8276  mptelixpg  8723  resixpfo  8724  bnd  9650  kmlem12  9917  lbzbi  12676  r19.29uz  15062  caubnd  15070  alzdvds  16029  ptclsg  22766  isucn2  23431  fusgreghash2wsp  28702  omssubadd  32267  subgrwlk  33094  dfon2lem8  33766  fvineqsneq  35583  dford3lem2  40849  neik0pk1imk0  41657  grur1cld  41850  mnuprdlem4  41893  mnurndlem1  41899