![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ralimdaa | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
ralimdaa.1 | ⊢ Ⅎ𝑥𝜑 |
ralimdaa.2 | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
ralimdaa | ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralimdaa.1 | . . 3 ⊢ Ⅎ𝑥𝜑 | |
2 | ralimdaa.2 | . . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) | |
3 | 2 | ex 414 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) |
4 | 1, 3 | ralrimi 3255 | . 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒)) |
5 | ralim 3087 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 → 𝜒) → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) | |
6 | 4, 5 | syl 17 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 Ⅎwnf 1786 ∈ wcel 2107 ∀wral 3062 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-12 2172 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-nf 1787 df-ral 3063 |
This theorem is referenced by: ralbida 3268 eltsk2g 10746 ptcnplem 23125 poimirlem26 36514 allbutfifvre 44391 climleltrp 44392 fnlimabslt 44395 limsupub2 44528 liminflbuz2 44531 xlimmnfvlem1 44548 xlimmnfvlem2 44549 xlimpnfvlem1 44552 xlimpnfvlem2 44553 stoweidlem61 44777 stoweid 44779 fourierdlem73 44895 smflimlem2 45488 |
Copyright terms: Public domain | W3C validator |