Theorem ralim 3073

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

Syntax hints:   → wi 4  ∀wral 3048

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 3049

This theorem is referenced by:  ralimdaa  3234  mpteqb  6957  tz7.49  8373  mptelixpg  8869  resixpfo  8870  bnd  9796  kmlem12  10064  lbzbi  12840  r19.29uz  15265  caubnd  15273  alzdvds  16238  ptclsg  23550  isucn2  24213  fusgreghash2wsp  30339  omssubadd  34385  trssfir1om  35194  r1omhfb  35195  trssfir1omregs  35204  r1omhfbregs  35205  subgrwlk  35248  dfon2lem8  35904  fvineqsneq  37529  dford3lem2  43184  neik0pk1imk0  44204  grur1cld  44389  mnuprdlem4  44432  mnurndlem1  44438