Theorem ralim 3087

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

Syntax hints:   → wi 4  ∀wral 3062

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 3063

This theorem is referenced by:  r19.30OLD  3122  ralimdaa  3258  mpteqb  7018  tz7.49  8445  mptelixpg  8929  resixpfo  8930  bnd  9887  kmlem12  10156  lbzbi  12920  r19.29uz  15297  caubnd  15305  alzdvds  16263  ptclsg  23119  isucn2  23784  fusgreghash2wsp  29591  omssubadd  33299  subgrwlk  34123  dfon2lem8  34762  fvineqsneq  36293  dford3lem2  41766  neik0pk1imk0  42798  grur1cld  42991  mnuprdlem4  43034  mnurndlem1  43040