Metamath Proof Explorer


Theorem tpnzd

Description: An unordered triple containing a set is not empty. (Contributed by Thierry Arnoux, 8-Apr-2019)

Ref Expression
Hypothesis tpnzd.1 ( 𝜑𝐴𝑉 )
Assertion tpnzd ( 𝜑 → { 𝐴 , 𝐵 , 𝐶 } ≠ ∅ )

Proof

Step Hyp Ref Expression
1 tpnzd.1 ( 𝜑𝐴𝑉 )
2 tpid1g ( 𝐴𝑉𝐴 ∈ { 𝐴 , 𝐵 , 𝐶 } )
3 ne0i ( 𝐴 ∈ { 𝐴 , 𝐵 , 𝐶 } → { 𝐴 , 𝐵 , 𝐶 } ≠ ∅ )
4 1 2 3 3syl ( 𝜑 → { 𝐴 , 𝐵 , 𝐶 } ≠ ∅ )