Theorem ralim 3103

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

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

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 3078

This theorem is used by:  ralimdaa  3264  mpteqb  7011  tz7.49  8448  mptelixpg  8956  resixpfo  8957  bnd  9948  kmlem12  10233  lbzbi  13056  r19.29uz  15511  caubnd  15519  alzdvds  16483  ptclsg  23927  isucn2  24590  subgrwlk  30262  fusgreghash2wsp  30932  omssubadd  34925  trssfir1om  35726  r1omhfb  35727  trssfir1omregs  35787  r1omhfbregs  35788  dfon2lem8  36532  fvineqsneq  38315  dford3lem2  44013  neik0pk1imk0  45032  grur1cld  45215  mnuprdlem4  45244  mnurndlem1  45250