Metamath Proof Explorer


Syntax definition cmitp

Description: The interpretation function of the model.

Ref Expression
Assertion cmitp class mItp