Theorem ralimdaa 3259

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	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
3	2	ex 412	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
4	1, 3	ralrimi 3256	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒))
5		ralim 3085	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 → 𝜒) → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))
6	4, 5	syl 17	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 395  Ⅎwnf 1782   ∈ wcel 2107  ∀wral 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-12 2176

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-nf 1783  df-ral 3061

This theorem is referenced by:  ralbida  3269  eltsk2g  10792  ptcnplem  23630  poimirlem26  37654  allbutfifvre  45695  climleltrp  45696  fnlimabslt  45699  limsupub2  45832  liminflbuz2  45835  xlimmnfvlem1  45852  xlimmnfvlem2  45853  xlimpnfvlem1  45856  xlimpnfvlem2  45857  stoweidlem61  46081  stoweid  46083  fourierdlem73  46199  smflimlem2  46792