Theorem ralim 2932

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

Syntax hints:   → wi 4  ∀wral 2896

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

This theorem depends on definitions:  df-bi 196  df-ral 2901

This theorem is referenced by:  ralimdaa  2941  r19.30  3063  trint  4696  mpteqb  6207  tz7.49  7427  mptelixpg  7831  resixpfo  7832  bnd  8638  kmlem12  8866  lbzbi  11652  r19.29uz  13938  caubnd  13946  alzdvds  14880  ptclsg  21228  isucn2  21893  usgreghash2spot  26596  omssubadd  29689  dfon2lem8  30939  dford3lem2  36612  neik0pk1imk0  37365  fusgreghash2wsp  41502