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 125 | 1 ⊢ (𝜑 ↔ 𝜑) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: biidd 171 an21 468 3anbi1i 1185 3anbi2i 1186 3anbi3i 1187 trubitru 1410 falbifal 1413 eqid 2170 abid2 2291 abid2f 2338 ceqsexg 2858 nnwetri 6893 exmidontriimlem3 7200 fsum2d 11398 fprod2d 11586 isstructim 12430 |
Copyright terms: Public domain | W3C validator |