Metamath Proof Explorer

Theorem thinccatd

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

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

Proof

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