Theorem ralim 3107

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 23	. 2 ⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜓))
2	1	ral2imi 3106	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓))

This proof depends on syntax axioms:   → wi 4  ∀wral 3081

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ral 3082

This theorem is used by:  ralimdaa  3268  mpteqb  7013  tz7.49  8434  mptelixpg  8935  resixpfo  8936  bnd  9887  kmlem12  10157  lbzbi  12971  r19.29uz  15421  caubnd  15429  alzdvds  16395  ptclsg  23801  isucn2  24464  fusgreghash2wsp  30718  omssubadd  34714  trssfir1om  35524  r1omhfb  35525  trssfir1omregs  35565  r1omhfbregs  35566  subgrwlk  35637  dfon2lem8  36293  fvineqsneq  38091  dford3lem2  43787  neik0pk1imk0  44806  grur1cld  44989  mnuprdlem4  45018  mnurndlem1  45024