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

Metamath Proof Explorer

Theorem termcthind

Description: A terminal category is a thin category (deduction form). (Contributed by Zhi Wang, 16-Oct-2025)

Ref Expression
Hypothesis termcthind.c ⊢ ( 𝜑 → 𝐶 ∈ TermCat )
Assertion termcthind ( 𝜑 → 𝐶 ∈ ThinCat )

Proof

Step Hyp Ref Expression
1 termcthind.c ⊢ ( 𝜑 → 𝐶 ∈ TermCat )
2 termcthin ⊢ ( 𝐶 ∈ TermCat → 𝐶 ∈ ThinCat )
3 1 2 syl ⊢ ( 𝜑 → 𝐶 ∈ ThinCat )