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  3230  mpteqb  6953  tz7.49  8374  mptelixpg  8869  resixpfo  8870  bnd  9807  kmlem12  10075  lbzbi  12856  r19.29uz  15277  caubnd  15285  alzdvds  16250  ptclsg  23519  isucn2  24183  fusgreghash2wsp  30301  omssubadd  34287  subgrwlk  35124  dfon2lem8  35783  fvineqsneq  37405  dford3lem2  43020  neik0pk1imk0  44040  grur1cld  44225  mnuprdlem4  44268  mnurndlem1  44274