Theorem ralim 3086

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

Syntax hints:   → wi 4  ∀wral 3061

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

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

This theorem is referenced by:  r19.30OLD  3121  ralimdaa  3260  mpteqb  7035  tz7.49  8485  mptelixpg  8975  resixpfo  8976  bnd  9932  kmlem12  10202  lbzbi  12978  r19.29uz  15389  caubnd  15397  alzdvds  16357  ptclsg  23623  isucn2  24288  fusgreghash2wsp  30357  omssubadd  34302  subgrwlk  35137  dfon2lem8  35791  fvineqsneq  37413  dford3lem2  43039  neik0pk1imk0  44060  grur1cld  44251  mnuprdlem4  44294  mnurndlem1  44300