df-ja - brismu bridi

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

Definition df-ja 190

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 191 jari 192