![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nfsb | Unicode version |
Description: If ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nfsb.1 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nfsb |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfsb.1 |
. . . 4
![]() ![]() ![]() ![]() | |
2 | 1 | nfsbxy 1916 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | nfsbxy 1916 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | ax-17 1507 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 4 | sbco2vh 1919 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5 | nfbii 1450 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 3, 6 | mpbi 144 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-10 1484 ax-11 1485 ax-i12 1486 ax-bndl 1487 ax-4 1488 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 |
This theorem depends on definitions: df-bi 116 df-nf 1438 df-sb 1737 |
This theorem is referenced by: nfsbv 1921 hbsb 1923 sbco2yz 1937 sbcomxyyz 1946 hbsbd 1958 nfsb4or 1999 sb8eu 2013 nfeu 2019 cbvab 2264 cbvralf 2651 cbvrexf 2652 cbvreu 2655 cbvralsv 2671 cbvrexsv 2672 cbvrab 2687 cbvreucsf 3069 cbvrabcsf 3070 cbvopab1 4009 cbvmptf 4030 cbvmpt 4031 ralxpf 4693 rexxpf 4694 cbviota 5101 sb8iota 5103 cbvriota 5748 dfoprab4f 6099 |
Copyright terms: Public domain | W3C validator |