Theorem ralim 3069

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

Syntax hints:   → wi 4  ∀wral 3044

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 3045

This theorem is referenced by:  ralimdaa  3238  mpteqb  6987  tz7.49  8413  mptelixpg  8908  resixpfo  8909  bnd  9845  kmlem12  10115  lbzbi  12895  r19.29uz  15317  caubnd  15325  alzdvds  16290  ptclsg  23502  isucn2  24166  fusgreghash2wsp  30267  omssubadd  34291  subgrwlk  35119  dfon2lem8  35778  fvineqsneq  37400  dford3lem2  43016  neik0pk1imk0  44036  grur1cld  44221  mnuprdlem4  44264  mnurndlem1  44270