![]() |
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 1783 | . 2 ⊢ (∃𝑥𝜑 → ∀𝑥𝜑) |
3 | 2 | 19.23bi 2179 | 1 ⊢ (𝜑 → ∀𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1531 Ⅎwnf 1777 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-12 2166 |
This theorem depends on definitions: df-bi 206 df-ex 1774 df-nf 1778 |
This theorem is referenced by: 19.3 2190 alimd 2200 alrimi 2201 eximd 2204 nexd 2209 albid 2210 exbid 2211 hbs1 2260 hba1 2282 hban 2289 hb3an 2290 nfal 2311 hbex 2313 nfsbv 2318 cbv3v 2325 cbv3 2390 equs45f 2452 nfs1 2481 sb6f 2490 hbsb 2517 hbab1 2711 nfsab 2715 nfsabg 2716 nfcrii 2885 ralrimi 3244 hbra1 3288 nfralw 3298 bnj1316 34582 bnj1379 34592 bnj1468 34608 bnj958 34702 bnj981 34712 bnj1014 34723 bnj1128 34752 bnj1204 34774 bnj1279 34780 bnj1398 34796 bnj1408 34798 bnj1444 34805 bnj1445 34806 bnj1446 34807 bnj1447 34808 bnj1448 34809 bnj1449 34810 bnj1463 34817 bnj1312 34820 bnj1518 34826 bnj1519 34827 bnj1520 34828 bnj1525 34831 bj-cbv2v 36406 bj-equs45fv 36419 mpobi123f 37766 |
Copyright terms: Public domain | W3C validator |