kc - Higher-Order Logic Explorer

	Higher-Order Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > HOLE Home > Th. List > kc		Unicode version

Syntax Definition kc 5

Description: A combination (function application).

**Hypotheses**
Ref	Expression
tf	term
tt	term

**Assertion**
Ref	Expression
kc	term

This syntax is primitive. The first axiom using it is ax-jca 17.

Colors of variables: type var term