![]() |
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 412 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) |
4 | 1, 3 | ralrimi 3253 | . 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒)) |
5 | ralim 3085 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 → 𝜒) → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) | |
6 | 4, 5 | syl 17 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 Ⅎwnf 1784 ∈ wcel 2105 ∀wral 3060 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-12 2170 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1781 df-nf 1785 df-ral 3061 |
This theorem is referenced by: ralbida 3266 eltsk2g 10749 ptcnplem 23346 poimirlem26 36818 allbutfifvre 44691 climleltrp 44692 fnlimabslt 44695 limsupub2 44828 liminflbuz2 44831 xlimmnfvlem1 44848 xlimmnfvlem2 44849 xlimpnfvlem1 44852 xlimpnfvlem2 44853 stoweidlem61 45077 stoweid 45079 fourierdlem73 45195 smflimlem2 45788 |
Copyright terms: Public domain | W3C validator |