Metamath Proof Explorer


Syntax definition cphtpc

Description: Extend class notation with the path homotopy relation.

Ref Expression
Assertion cphtpc
class ~=ph