brismu bridi		< Previous   Next > Nearby theorems
Mirrors  >  Home  >   Home  >  Th. List  >  df-ja

---

Definition df-ja 145

Description: Definition of {ja} in terms of {ga}. From example 12.2-5 of [CLL] p. 14.

Assertion

Ref	Expression
df-ja	⊢ go ko'a bu'a ja bu'e ko'e gi ga 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:  jai  146  jari  147

Copyright terms: Public domain

W3C validator