![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfsb | Structured version Visualization version Unicode version |
Description: If ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nfsb.1 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nfsb |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | axc16nf 2027 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | nfsb.1 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 2 | nfsb4 2219 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | pm2.61i 168 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 |
This theorem depends on definitions: df-bi 189 df-an 373 df-ex 1664 df-nf 1668 df-sb 1798 |
This theorem is referenced by: hbsb 2270 sb10f 2285 2sb8e 2296 sb8eu 2332 2mo 2380 cbvralf 3013 cbvreu 3017 cbvralsv 3030 cbvrexsv 3031 cbvrab 3043 cbvreucsf 3397 cbvrabcsf 3398 cbvopab1 4473 cbvmptf 4493 cbvmpt 4494 ralxpf 4981 cbviota 5551 sb8iota 5553 cbvriota 6262 dfoprab4f 6851 mo5f 28120 ax11-pm2 31438 2sb5nd 36927 |
Copyright terms: Public domain | W3C validator |