| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > nf5ri | Structured version Visualization version GIF version | ||
| Description: Consequence of the definition of not-free. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 15-Mar-2023.) |
| Ref | Expression |
|---|---|
| nf5ri.1 | ⊢ Ⅎ𝑥𝜑 |
| Ref | Expression |
|---|---|
| nf5ri | ⊢ (𝜑 → ∀𝑥𝜑) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nf5ri.1 | . . 3 ⊢ Ⅎ𝑥𝜑 | |
| 2 | 1 | nfri 1789 | . 2 ⊢ (∃𝑥𝜑 → ∀𝑥𝜑) |
| 3 | 2 | 19.23bi 2191 | 1 ⊢ (𝜑 → ∀𝑥𝜑) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∀wal 1538 Ⅎwnf 1783 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-12 2177 |
| This theorem depends on definitions: df-bi 207 df-ex 1780 df-nf 1784 |
| This theorem is referenced by: 19.3 2202 alimd 2212 alrimi 2213 eximd 2216 nexd 2221 albid 2222 exbid 2223 hbs1 2274 hba1 2293 hban 2300 hb3an 2301 nfal 2323 hbex 2325 nfsbv 2330 cbv3v 2337 cbv3 2402 equs45f 2464 nfs1 2493 sb6f 2502 hbsb 2529 hbab1 2723 nfsab 2727 nfsabg 2728 nfcrii 2900 ralrimi 3257 hbra1 3301 nfralw 3311 bnj1316 34834 bnj1379 34844 bnj1468 34860 bnj958 34954 bnj981 34964 bnj1014 34975 bnj1128 35004 bnj1204 35026 bnj1279 35032 bnj1398 35048 bnj1408 35050 bnj1444 35057 bnj1445 35058 bnj1446 35059 bnj1447 35060 bnj1448 35061 bnj1449 35062 bnj1463 35069 bnj1312 35072 bnj1518 35078 bnj1519 35079 bnj1520 35080 bnj1525 35083 bj-cbv2v 36799 bj-equs45fv 36812 mpobi123f 38169 |
| Copyright terms: Public domain | W3C validator |