Theorem ralim 3105

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

Syntax hints:   → wi 4  ∀wral 3079

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

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

This theorem is referenced by:  ralimdaa  3266  mpteqb  7011  tz7.49  8433  mptelixpg  8934  resixpfo  8935  bnd  9879  kmlem12  10146  lbzbi  12961  r19.29uz  15404  caubnd  15412  alzdvds  16379  ptclsg  23753  isucn2  24416  fusgreghash2wsp  30670  omssubadd  34671  trssfir1om  35488  r1omhfb  35489  trssfir1omregs  35530  r1omhfbregs  35531  subgrwlk  35605  dfon2lem8  36261  fvineqsneq  38039  dford3lem2  43737  neik0pk1imk0  44756  grur1cld  44939  mnuprdlem4  44968  mnurndlem1  44974