Theorem ralim 3101

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

Syntax hints:   → wi 4  ∀wral 3075

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

This theorem depends on definitions:  df-bi 209  df-ral 3076

This theorem is referenced by:  ralimdaa  3262  mpteqb  6990  tz7.49  8410  mptelixpg  8911  resixpfo  8912  bnd  9844  kmlem12  10112  lbzbi  12931  r19.29uz  15369  caubnd  15377  alzdvds  16345  ptclsg  23663  isucn2  24326  fusgreghash2wsp  30497  omssubadd  34558  trssfir1om  35368  r1omhfb  35369  trssfir1omregs  35393  r1omhfbregs  35394  subgrwlk  35443  dfon2lem8  36099  fvineqsneq  37867  dford3lem2  43565  neik0pk1imk0  44584  grur1cld  44769  mnuprdlem4  44812  mnurndlem1  44818