Theorem ralim 3111

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

Syntax hints:   → wi 4  ∀wral 3085

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

This theorem depends on definitions:  df-bi 210  df-ral 3086

This theorem is referenced by:  ralimdaa  3272  mpteqb  7007  tz7.49  8428  mptelixpg  8929  resixpfo  8930  bnd  9874  kmlem12  10141  lbzbi  12956  r19.29uz  15398  caubnd  15406  alzdvds  16374  ptclsg  23737  isucn2  24400  fusgreghash2wsp  30626  omssubadd  34631  trssfir1om  35443  r1omhfb  35444  trssfir1omregs  35468  r1omhfbregs  35469  subgrwlk  35519  dfon2lem8  36175  fvineqsneq  37941  dford3lem2  43639  neik0pk1imk0  44658  grur1cld  44841  mnuprdlem4  44870  mnurndlem1  44876