Theorem ralimdaa 3240

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-Sep-2003.) (Proof shortened by Wolf Lammen, 29-Dec-2019.)

Hypotheses

Ref	Expression
ralimdaa.1	⊢ Ⅎ𝑥𝜑
ralimdaa.2	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))

Assertion

Ref	Expression
ralimdaa	⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Proof of Theorem ralimdaa

Step	Hyp	Ref	Expression
1		ralimdaa.1	. . 3 ⊢ Ⅎ𝑥𝜑
2		ralimdaa.2	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
3	1, 2	ralrimia 3238	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒))
4		ralim 3079	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 → 𝜒) → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))
5	3, 4	syl 17	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 396  Ⅎwnf 1790   ∈ wcel 2119  ∀wral 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-12 2189

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-nf 1791  df-ral 3054

This theorem is referenced by:  ralbida  3250  eltsk2g  10665  ptcnplem  23604  poimirlem26  38013  allbutfifvre  46118  climleltrp  46119  fnlimabslt  46122  limsupub2  46255  liminflbuz2  46258  xlimmnfvlem1  46275  xlimmnfvlem2  46276  xlimpnfvlem1  46279  xlimpnfvlem2  46280  stoweidlem61  46504  stoweid  46506  fourierdlem73  46622  smflimlem2  47215