![]() |
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 2188 | . 2 ⊢ (Ⅎ𝑥𝜓 → (𝜓 → ∀𝑥𝜓)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1540 Ⅎwnf 1786 |
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-ex 1783 df-nf 1787 |
This theorem is referenced by: spimedv 2191 alrimdd 2208 nf5di 2282 hbnt 2291 hbimd 2295 dvelimhw 2342 dveeq2 2378 dveeq1 2380 axc9 2382 spimed 2388 dvelimh 2450 abidnf 3699 eusvnfb 5392 axrepnd 10589 axacndlem4 10605 bj-cbv2v 35676 bj-elgab 35819 wl-nfeqfb 36405 |
Copyright terms: Public domain | W3C validator |