Theorem ralim 3092

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

Syntax hints:   → wi 4  ∀wral 3067

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

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

This theorem is referenced by:  r19.30OLD  3127  ralimdaa  3266  mpteqb  7048  tz7.49  8501  mptelixpg  8993  resixpfo  8994  bnd  9961  kmlem12  10231  lbzbi  13001  r19.29uz  15399  caubnd  15407  alzdvds  16368  ptclsg  23644  isucn2  24309  fusgreghash2wsp  30370  omssubadd  34265  subgrwlk  35100  dfon2lem8  35754  fvineqsneq  37378  dford3lem2  42984  neik0pk1imk0  44009  grur1cld  44201  mnuprdlem4  44244  mnurndlem1  44250