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  29622  omssubadd  33330  subgrwlk  34154  dfon2lem8  34793  fvineqsneq  36341  dford3lem2  41814  neik0pk1imk0  42846  grur1cld  43039  mnuprdlem4  43082  mnurndlem1  43088