Theorem ralim 3102

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

This proof depends on syntax axioms:   → wi 4  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841

This proof depends on definitions:  df-bi 210  df-ral 3077

This theorem is used by:  ralimdaa  3263  mpteqb  7014  tz7.49  8459  mptelixpg  8967  resixpfo  8968  bnd  9959  kmlem12  10244  lbzbi  13067  r19.29uz  15524  caubnd  15532  alzdvds  16496  ptclsg  23940  isucn2  24603  subgrwlk  30275  fusgreghash2wsp  30945  trssfir1om  35790  r1omhfb  35791  trssfir1omregs  35861  r1omhfbregs  35862  dfon2lem8  36645  fvineqsneq  38429  dford3lem2  44128  neik0pk1imk0  45141  grur1cld  45324  mnuprdlem4  45353  mnurndlem1  45359