![]() |
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 1919 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | nfsbxy 1919 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | ax-17 1503 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 4 | sbco2vh 1922 |
. . 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 1481 ax-10 1482 ax-11 1483 ax-i12 1484 ax-bndl 1486 ax-4 1487 ax-17 1503 ax-i9 1507 ax-ial 1511 ax-i5r 1512 |
This theorem depends on definitions: df-bi 116 df-nf 1438 df-sb 1740 |
This theorem is referenced by: hbsb 1926 sbco2yz 1940 sbcomxyyz 1949 hbsbd 1959 nfsb4or 1998 sb8eu 2016 nfeu 2022 cbvab 2278 cbvralf 2671 cbvrexf 2672 cbvreu 2675 cbvralsv 2691 cbvrexsv 2692 cbvrab 2707 cbvreucsf 3091 cbvrabcsf 3092 cbvopab1 4033 cbvmptf 4054 cbvmpt 4055 ralxpf 4725 rexxpf 4726 cbviota 5133 sb8iota 5135 cbvriota 5780 dfoprab4f 6131 |
Copyright terms: Public domain | W3C validator |