kc - Higher-Order Logic Explorer

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

Syntax Definition kc 5

Description: A combination (function application).

**Hypotheses**
Ref	Expression
tf	term F
tt	term T

**Assertion**
Ref	Expression
kc	term (FT)

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

Colors of variables: type var term