Theorem ralim 3094

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

Syntax hints:   → wi 4  ∀wral 3070

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 210  df-ral 3075

This theorem is referenced by:  ralimdaa  3145  r19.30  3258  mpteqb  6778  tz7.49  8091  mptelixpg  8517  resixpfo  8518  bnd  9354  kmlem12  9621  lbzbi  12376  r19.29uz  14758  caubnd  14766  alzdvds  15721  ptclsg  22315  isucn2  22980  fusgreghash2wsp  28222  omssubadd  31786  subgrwlk  32610  dfon2lem8  33282  fvineqsneq  35109  dford3lem2  40341  neik0pk1imk0  41123  grur1cld  41313  mnuprdlem4  41356  mnurndlem1  41362