Theorem ralim 3077

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

Syntax hints:   → wi 4  ∀wral 3051

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

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

This theorem is referenced by:  ralimdaa  3238  mpteqb  6967  tz7.49  8384  mptelixpg  8883  resixpfo  8884  bnd  9816  kmlem12  10084  lbzbi  12886  r19.29uz  15313  caubnd  15321  alzdvds  16289  ptclsg  23580  isucn2  24243  fusgreghash2wsp  30408  omssubadd  34444  trssfir1om  35255  r1omhfb  35256  trssfir1omregs  35280  r1omhfbregs  35281  subgrwlk  35314  dfon2lem8  35970  fvineqsneq  37728  dford3lem2  43455  neik0pk1imk0  44474  grur1cld  44659  mnuprdlem4  44702  mnurndlem1  44708