Metamath Proof Explorer

Theorem thinccd

Description: A thin category is a category (deduction form). (Contributed by Zhi Wang, 24-Sep-2024)

Ref Expression
Hypothesis thinccd.c 
|- ( ph -> C e. ThinCat )
Assertion thinccd 
|- ( ph -> C e. Cat )

Proof

Step Hyp Ref Expression
1 thinccd.c 
 |-  ( ph -> C e. ThinCat )
2 thincc 
 |-  ( C e. ThinCat -> C e. Cat )
3 1 2 syl 
 |-  ( ph -> C e. Cat )