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 2195 | . 2 ⊢ (Ⅎ𝑥𝜓 → (𝜓 → ∀𝑥𝜓)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1540 Ⅎwnf 1790 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-12 2179 |
This theorem depends on definitions: df-bi 210 df-ex 1787 df-nf 1791 |
This theorem is referenced by: spimedv 2199 alrimdd 2216 nf5di 2289 hbnt 2298 hbimd 2302 dvelimhw 2348 dveeq2 2378 dveeq1 2380 axc9 2382 spimed 2388 dvelimh 2450 abidnf 3602 eusvnfb 5260 axrepnd 10094 axacndlem4 10110 bj-cbv2v 34623 bj-elgab 34770 wl-nfeqfb 35338 |
Copyright terms: Public domain | W3C validator |