![]() |
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 1480 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5 | trud 1252 |
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 1336 ax-gen 1338 ax-4 1400 ax-ial 1427 ax-i5r 1428 |
This theorem depends on definitions: df-bi 110 df-tru 1246 df-nf 1350 |
This theorem is referenced by: sb8eu 1913 nfeuv 1918 bm1.1 2025 abbi 2151 nfeq 2185 cleqf 2201 sbhypf 2603 ceqsexg 2672 elabgt 2684 elabgf 2685 copsex2t 3982 copsex2g 3983 opelopabsb 3997 opeliunxp2 4476 ralxpf 4482 rexxpf 4483 cbviota 4872 sb8iota 4874 fmptco 5330 nfiso 5446 dfoprab4f 5819 bdsepnfALT 10009 strcollnfALT 10111 |
Copyright terms: Public domain | W3C validator |