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 2193 | . 2 ⊢ (Ⅎ𝑥𝜓 → (𝜓 → ∀𝑥𝜓)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1535 Ⅎwnf 1784 |
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 1911 ax-6 1970 ax-7 2015 ax-12 2177 |
This theorem depends on definitions: df-bi 209 df-ex 1781 df-nf 1785 |
This theorem is referenced by: spimedv 2197 alrimdd 2214 nf5di 2293 hbnt 2302 hbimd 2306 dvelimhw 2366 dveeq2 2396 dveeq1 2398 axc9 2400 spimed 2406 cbv2OLD 2427 dvelimh 2472 abidnf 3694 eusvnfb 5294 axrepnd 10016 axacndlem4 10032 bj-cbv2v 34120 wl-nfeqfb 34791 |
Copyright terms: Public domain | W3C validator |