![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nfbi | Unicode version |
Description: If ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nfbi.1 |
![]() ![]() ![]() ![]() |
nfbi.2 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nfbi |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfbi.1 |
. . . 4
![]() ![]() ![]() ![]() | |
2 | 1 | a1i 9 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | nfbi.2 |
. . . 4
![]() ![]() ![]() ![]() | |
4 | 3 | a1i 9 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | nfbid 1477 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5 | trud 1251 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1333 ax-gen 1335 ax-4 1397 ax-ial 1424 ax-i5r 1425 |
This theorem depends on definitions: df-bi 110 df-tru 1245 df-nf 1347 |
This theorem is referenced by: sb8eu 1910 nfeuv 1915 bm1.1 2022 abbi 2148 nfeq 2182 cleqf 2198 sbhypf 2597 ceqsexg 2666 elabgt 2678 elabgf 2679 copsex2t 3973 copsex2g 3974 opelopabsb 3988 opeliunxp2 4419 ralxpf 4425 rexxpf 4426 cbviota 4815 sb8iota 4817 fmptco 5273 nfiso 5389 dfoprab4f 5761 bdsepnfALT 9344 strcollnfALT 9446 |
Copyright terms: Public domain | W3C validator |