Theorem ralimdaa 3272

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 3270	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒))
4		ralim 3111	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 → 𝜒) → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))
5	3, 4	syl 18	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 400  Ⅎwnf 1810   ∈ wcel 2149  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-12 2219

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-nf 1811  df-ral 3086

This theorem is referenced by:  ralbida  3282  eltsk2g  10735  ptcnplem  23746  poimirlem26  38184  allbutfifvre  46280  climleltrp  46281  fnlimabslt  46284  limsupub2  46417  liminflbuz2  46420  xlimmnfvlem1  46437  xlimmnfvlem2  46438  xlimpnfvlem1  46441  xlimpnfvlem2  46442  stoweidlem61  46666  stoweid  46668  fourierdlem73  46784  smflimlem2  47377