This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝐶 ∈ ThinCat )
Assertion thinccd ( 𝜑 → 𝐶 ∈ Cat )

Proof

Step Hyp Ref Expression
1 thinccd.c ⊢ ( 𝜑 → 𝐶 ∈ ThinCat )
2 thincc ⊢ ( 𝐶 ∈ ThinCat → 𝐶 ∈ Cat )
3 1 2 syl ⊢ ( 𝜑 → 𝐶 ∈ Cat )