Theorem ralim 3072

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

Syntax hints:   → wi 4  ∀wral 3047

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

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

This theorem is referenced by:  ralimdaa  3233  mpteqb  6943  tz7.49  8359  mptelixpg  8854  resixpfo  8855  bnd  9780  kmlem12  10048  lbzbi  12829  r19.29uz  15253  caubnd  15261  alzdvds  16226  ptclsg  23525  isucn2  24188  fusgreghash2wsp  30310  omssubadd  34305  trssfir1om  35114  r1omhfb  35115  trssfir1omregs  35124  r1omhfbregs  35125  subgrwlk  35168  dfon2lem8  35824  fvineqsneq  37446  dford3lem2  43060  neik0pk1imk0  44080  grur1cld  44265  mnuprdlem4  44308  mnurndlem1  44314