Theorem ralim 3106

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 23	. 2 ⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜓))
2	1	ral2imi 3105	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 𝜓))

This proof depends on syntax axioms:   → wi 4  ∀wral 3080

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ral 3081

This theorem is used by:  ralimdaa  3267  mpteqb  7044  tz7.49  8493  mptelixpg  9001  resixpfo  9002  bnd  9992  kmlem12  10279  lbzbi  13103  r19.29uz  15562  caubnd  15570  alzdvds  16534  ptclsg  23989  isucn2  24652  subgrwlk  30326  fusgreghash2wsp  30996  trssfihf  35860  eqhf  35861  trssfihfregs  35945  eqhfregs  35946  dfon2lem8  36767  fvineqsneq  38603  dford3lem2  44300  neik0pk1imk0  45308  grur1cld  45491  mnuprdlem4  45520  mnurndlem1  45526