Theorem ralim 3082

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

Syntax hints:   → wi 4  ∀wral 3063

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

This theorem depends on definitions:  df-bi 206  df-ral 3068

This theorem is referenced by:  ralimdaa  3140  r19.30OLD  3266  mpteqb  6876  tz7.49  8246  mptelixpg  8681  resixpfo  8682  bnd  9581  kmlem12  9848  lbzbi  12605  r19.29uz  14990  caubnd  14998  alzdvds  15957  ptclsg  22674  isucn2  23339  fusgreghash2wsp  28603  omssubadd  32167  subgrwlk  32994  dfon2lem8  33672  fvineqsneq  35510  dford3lem2  40765  neik0pk1imk0  41546  grur1cld  41739  mnuprdlem4  41782  mnurndlem1  41788