![]() |
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 1599 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5 | mptru 1373 |
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 106 ax-ia2 107 ax-ia3 108 ax-5 1458 ax-gen 1460 ax-4 1521 ax-ial 1545 ax-i5r 1546 |
This theorem depends on definitions: df-bi 117 df-tru 1367 df-nf 1472 |
This theorem is referenced by: sb8eu 2051 nfeuv 2056 bm1.1 2174 abbi 2303 nfeq 2340 cleqf 2357 sbhypf 2801 ceqsexg 2880 elabgt 2893 elabgf 2894 copsex2t 4263 copsex2g 4264 opelopabsb 4278 opeliunxp2 4785 ralxpf 4791 rexxpf 4792 cbviota 5201 sb8iota 5203 fmptco 5703 nfiso 5828 dfoprab4f 6219 opeliunxp2f 6264 xpf1o 6873 bdsepnfALT 15119 |
Copyright terms: Public domain | W3C validator |