Theorem ralim 3102

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

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

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 3077

This theorem is used by:  ralimdaa  3263  mpteqb  7006  tz7.49  8434  mptelixpg  8942  resixpfo  8943  bnd  9894  kmlem12  10164  lbzbi  12985  r19.29uz  15438  caubnd  15446  alzdvds  16410  ptclsg  23841  isucn2  24504  subgrwlk  30148  fusgreghash2wsp  30818  omssubadd  34811  trssfir1om  35621  r1omhfb  35622  trssfir1omregs  35662  r1omhfbregs  35663  dfon2lem8  36367  fvineqsneq  38166  dford3lem2  43868  neik0pk1imk0  44887  grur1cld  45070  mnuprdlem4  45099  mnurndlem1  45105