Nearby theorems
|
|
brismu bridi |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > Home > Th. List > df-go | |||
| Description: Definition of {go} in terms of {ganai} and {ge}. This is the standard definition of the biconditional connective in higher-order intuitionistic logic. This can be justified intuitionistically; see theorem df-bi along with bijust from [ILE] p. 0. |
| Ref | Expression |
|---|---|
| df-go | ⊢ ge ganai go broda gi brode gi ge ganai broda gi brode gi ganai brode gi broda gi ganai ge ganai broda gi brode gi ganai brode gi broda gi go broda gi brode |
| Copyright terms: Public domain | W3C validator |