![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > biid | Unicode version |
Description: Principle of identity for logical equivalence. Theorem *4.2 of [WhiteheadRussell] p. 117. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
biid |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1, 1 | impbii 126 |
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-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: biidd 172 an21 471 3anbi1i 1192 3anbi2i 1193 3anbi3i 1194 trubitru 1426 falbifal 1429 eqid 2193 abid2 2314 abid2f 2362 ceqsexg 2888 nnwetri 6963 exmidontriimlem3 7273 fsum2d 11565 fprod2d 11753 isstructim 12619 lmodvscl 13779 |
Copyright terms: Public domain | W3C validator |