New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE 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 180 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wb 176 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 177 |
This theorem is referenced by: biidd 228 pm5.19 349 3anbi1i 1142 3anbi2i 1143 3anbi3i 1144 trujust 1318 tru 1321 trubitru 1350 falbifal 1353 hadcoma 1388 hadcomb 1389 hadnot 1393 cadcomb 1396 eqid 2353 abid2 2470 abid2f 2514 ceqsexg 2970 opksnelsik 4265 restxp 5786 oqelins4 5794 |
Copyright terms: Public domain | W3C validator |