![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nf5rd | Structured version Visualization version GIF version |
Description: Consequence of the definition of not-free in a context. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Ref | Expression |
---|---|
nf5rd.1 | ⊢ (𝜑 → Ⅎ𝑥𝜓) |
Ref | Expression |
---|---|
nf5rd | ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nf5rd.1 | . 2 ⊢ (𝜑 → Ⅎ𝑥𝜓) | |
2 | nf5r 2191 | . 2 ⊢ (Ⅎ𝑥𝜓 → (𝜓 → ∀𝑥𝜓)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1536 Ⅎwnf 1785 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-12 2175 |
This theorem depends on definitions: df-bi 210 df-ex 1782 df-nf 1786 |
This theorem is referenced by: spimedv 2195 alrimdd 2212 nf5di 2289 hbnt 2298 hbimd 2302 dvelimhw 2355 dveeq2 2385 dveeq1 2387 axc9 2389 spimed 2395 cbv2OLD 2416 dvelimh 2461 abidnf 3642 eusvnfb 5259 axrepnd 10005 axacndlem4 10021 bj-cbv2v 34235 wl-nfeqfb 34941 |
Copyright terms: Public domain | W3C validator |