![]() |
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 1548 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5 | mptru 1321 |
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 105 ax-ia2 106 ax-ia3 107 ax-5 1404 ax-gen 1406 ax-4 1468 ax-ial 1495 ax-i5r 1496 |
This theorem depends on definitions: df-bi 116 df-tru 1315 df-nf 1418 |
This theorem is referenced by: sb8eu 1986 nfeuv 1991 bm1.1 2098 abbi 2226 nfeq 2261 cleqf 2277 sbhypf 2704 ceqsexg 2781 elabgt 2793 elabgf 2794 copsex2t 4125 copsex2g 4126 opelopabsb 4140 opeliunxp2 4637 ralxpf 4643 rexxpf 4644 cbviota 5049 sb8iota 5051 fmptco 5538 nfiso 5659 dfoprab4f 6042 opeliunxp2f 6086 xpf1o 6688 bdsepnfALT 12766 strcollnfALT 12863 |
Copyright terms: Public domain | W3C validator |