Theorem ralim 3078

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

Syntax hints:   → wi 4  ∀wral 3052

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 3053

This theorem is referenced by:  ralimdaa  3239  mpteqb  6961  tz7.49  8377  mptelixpg  8876  resixpfo  8877  bnd  9807  kmlem12  10075  lbzbi  12877  r19.29uz  15304  caubnd  15312  alzdvds  16280  ptclsg  23590  isucn2  24253  fusgreghash2wsp  30423  omssubadd  34460  trssfir1om  35271  r1omhfb  35272  trssfir1omregs  35296  r1omhfbregs  35297  subgrwlk  35330  dfon2lem8  35986  fvineqsneq  37742  dford3lem2  43473  neik0pk1imk0  44492  grur1cld  44677  mnuprdlem4  44720  mnurndlem1  44726