Theorem ralim 3074

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

Syntax hints:   → wi 4  ∀wral 3049

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 3050

This theorem is referenced by:  ralimdaa  3235  mpteqb  6957  tz7.49  8373  mptelixpg  8868  resixpfo  8869  bnd  9795  kmlem12  10063  lbzbi  12844  r19.29uz  15268  caubnd  15276  alzdvds  16241  ptclsg  23540  isucn2  24203  fusgreghash2wsp  30329  omssubadd  34324  trssfir1om  35133  r1omhfb  35134  trssfir1omregs  35143  r1omhfbregs  35144  subgrwlk  35187  dfon2lem8  35843  fvineqsneq  37467  dford3lem2  43134  neik0pk1imk0  44154  grur1cld  44339  mnuprdlem4  44382  mnurndlem1  44388