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

---

Definition df-jonai 235

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

Assertion

Ref	Expression
df-jonai	⊢ go ko'a bu'a jonai bu'e ko'e gi gonai 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:  jonaii  236  jonairi  237

Copyright terms: Public domain

W3C validator