![]() |
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 2192 | . 2 ⊢ (Ⅎ𝑥𝜓 → (𝜓 → ∀𝑥𝜓)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1535 Ⅎwnf 1780 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-12 2175 |
This theorem depends on definitions: df-bi 207 df-ex 1777 df-nf 1781 |
This theorem is referenced by: spimedv 2195 alrimdd 2212 nf5di 2284 hbnt 2293 hbimd 2297 dvelimhw 2346 dveeq2 2381 dveeq1 2383 axc9 2385 spimed 2391 dvelimh 2453 abidnf 3711 eusvnfb 5399 axrepnd 10632 axacndlem4 10648 bj-cbv2v 36781 bj-elgab 36922 wl-nfeqfb 37517 |
Copyright terms: Public domain | W3C validator |