Theorem ralim 3162

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

Syntax hints:   → wi 4  ∀wral 3138

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

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

This theorem is referenced by:  ralimdaa  3217  r19.30  3338  r19.30OLD  3339  mpteqb  6786  tz7.49  8080  mptelixpg  8498  resixpfo  8499  bnd  9320  kmlem12  9586  lbzbi  12335  r19.29uz  14709  caubnd  14717  alzdvds  15669  ptclsg  22222  isucn2  22887  fusgreghash2wsp  28116  omssubadd  31558  subgrwlk  32379  dfon2lem8  33035  fvineqsneq  34692  dford3lem2  39622  neik0pk1imk0  40395  grur1cld  40566  mnuprdlem4  40609  mnurndlem1  40615