Theorem ralim 3076

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

Syntax hints:   → wi 4  ∀wral 3051

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

This theorem depends on definitions:  df-bi 207  df-ral 3052

This theorem is referenced by:  ralimdaa  3237  mpteqb  6960  tz7.49  8376  mptelixpg  8873  resixpfo  8874  bnd  9804  kmlem12  10072  lbzbi  12849  r19.29uz  15274  caubnd  15282  alzdvds  16247  ptclsg  23559  isucn2  24222  fusgreghash2wsp  30413  omssubadd  34457  trssfir1om  35267  r1omhfb  35268  trssfir1omregs  35292  r1omhfbregs  35293  subgrwlk  35326  dfon2lem8  35982  fvineqsneq  37617  dford3lem2  43269  neik0pk1imk0  44288  grur1cld  44473  mnuprdlem4  44516  mnurndlem1  44522