![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > biid | GIF 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: ↔ wb 105 |
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 1190 3anbi2i 1191 3anbi3i 1192 trubitru 1415 falbifal 1418 eqid 2177 abid2 2298 abid2f 2345 ceqsexg 2865 nnwetri 6914 exmidontriimlem3 7221 fsum2d 11438 fprod2d 11626 isstructim 12470 |
Copyright terms: Public domain | W3C validator |