Theorem termccd 49448

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

Hypothesis

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

Assertion

Ref	Expression
termccd	⊢ (𝜑 → 𝐶 ∈ Cat)

Proof of Theorem termccd

Step	Hyp	Ref	Expression
1		termcthind.c	. . 3 ⊢ (𝜑 → 𝐶 ∈ TermCat)
2	1	termcthind 49447	. 2 ⊢ (𝜑 → 𝐶 ∈ ThinCat)
3	2	thinccd 49392	1 ⊢ (𝜑 → 𝐶 ∈ Cat)

Syntax hints:   → wi 4   ∈ wcel 2109  Catccat 17631  TermCatctermc 49441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-nul 5263

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-mo 2534  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3756  df-dif 3919  df-un 3921  df-ss 3933  df-nul 4299  df-if 4491  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5110  df-iota 6466  df-fv 6521  df-ov 7392  df-thinc 49387  df-termc 49442

This theorem is referenced by:  termchomn0  49453  funcsetc1ocl  49465  funcsetc1o  49466  isinito2lem  49467  isinito3  49469  termcterm  49482  termcterm2  49483  termc2  49487  termcarweu  49497  diag1f1olem  49502  diag1f1o  49503  diag2f1olem  49505  diag2f1o  49506  diagffth  49507  diagciso  49508  diagcic  49509  termfucterm  49513  uobeqterm  49515  isinito4a  49517  setc1onsubc  49571