Metamath Proof Explorer


Syntax definition cmpps

Description: The set of provable pre-statements.

Ref Expression
Assertion cmpps class mPPSt