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

---

Definition df-jo 160

Description: Definition of {jo} in terms of {go}. By analogy with example 12.2-5 of [CLL] p. 14.

Assertion

Ref	Expression
df-jo	⊢ go ko'a bu'a jo bu'e ko'e gi go 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:  joi  161  jori  162

Copyright terms: Public domain

W3C validator