Theorem tpssd

Description: Deduction version of tpssi : An unordered triple of elements of a class is a subset of that class. (Contributed by Thierry Arnoux, 2-Nov-2025)

	Ref	Expression
Hypotheses	tpssd.1	⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )
	tpssd.2	⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
	tpssd.3	⊢ ( 𝜑 → 𝐶 ∈ 𝐷 )
Assertion	tpssd	⊢ ( 𝜑 → { 𝐴 , 𝐵 , 𝐶 } ⊆ 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		tpssd.1	⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )
2		tpssd.2	⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
3		tpssd.3	⊢ ( 𝜑 → 𝐶 ∈ 𝐷 )
4		tpssi	⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐷 ) → { 𝐴 , 𝐵 , 𝐶 } ⊆ 𝐷 )
5	1 2 3 4	syl3anc	⊢ ( 𝜑 → { 𝐴 , 𝐵 , 𝐶 } ⊆ 𝐷 )