wffMMJ2t - Higher-Order Logic Explorer

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

Syntax Definition wffMMJ2t 12

Description: Internal axiom for mmj2 use.

**Hypotheses**
Ref	Expression
hal	type
ta	term

**Assertion**
Ref	Expression
wffMMJ2t	wff

This syntax is primitive. The first axiom using it is ax-cb1 29.

Colors of variables: type var term