Home brismu bridi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >   Home  >  Th. List  >  df-naja
Definition df-naja 89
Description: Definition of {naja} in terms of {ganai}. By analogy with example 12.2-5 of [CLL] p. 14.
Assertion
Ref Expression
df-naja ⊢ go ko'a bu'a naja bu'e ko'e gi ganai ko'a bu'a ko'e gi ko'a bu'e ko'e
Distinct variable group:   bu'a ,bu'e
This definition is referenced by:  najai  90  najari  92
  Copyright terms: Public domain W3C validator