Theorem ralim 3078

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

Syntax hints:   → wi 4  ∀wral 3052

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

This theorem depends on definitions:  df-bi 207  df-ral 3053

This theorem is referenced by:  ralimdaa  3239  mpteqb  6969  tz7.49  8386  mptelixpg  8885  resixpfo  8886  bnd  9816  kmlem12  10084  lbzbi  12861  r19.29uz  15286  caubnd  15294  alzdvds  16259  ptclsg  23571  isucn2  24234  fusgreghash2wsp  30425  omssubadd  34477  trssfir1om  35286  r1omhfb  35287  trssfir1omregs  35311  r1omhfbregs  35312  subgrwlk  35345  dfon2lem8  36001  fvineqsneq  37664  dford3lem2  43381  neik0pk1imk0  44400  grur1cld  44585  mnuprdlem4  44628  mnurndlem1  44634