Theorem ralim 2977

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

Syntax hints:   → wi 4  ∀wral 2941

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

This theorem depends on definitions:  df-bi 197  df-ral 2946

This theorem is referenced by:  ralimdaa  2987  r19.30  3111  trint  4801  mpteqb  6338  tz7.49  7585  mptelixpg  7987  resixpfo  7988  bnd  8793  kmlem12  9021  lbzbi  11814  r19.29uz  14134  caubnd  14142  alzdvds  15089  ptclsg  21466  isucn2  22130  fusgreghash2wsp  27318  omssubadd  30490  dfon2lem8  31819  dford3lem2  37911  neik0pk1imk0  38662