Theorem ralim 3079

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

Syntax hints:   → wi 4  ∀wral 3053

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

This theorem depends on definitions:  df-bi 208  df-ral 3054

This theorem is referenced by:  ralimdaa  3240  mpteqb  6955  tz7.49  8374  mptelixpg  8873  resixpfo  8874  bnd  9807  kmlem12  10075  lbzbi  12877  r19.29uz  15304  caubnd  15312  alzdvds  16280  ptclsg  23598  isucn2  24261  fusgreghash2wsp  30426  omssubadd  34484  trssfir1om  35292  r1omhfb  35293  trssfir1omregs  35317  r1omhfbregs  35318  subgrwlk  35360  dfon2lem8  36016  fvineqsneq  37774  dford3lem2  43472  neik0pk1imk0  44491  grur1cld  44676  mnuprdlem4  44719  mnurndlem1  44725