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

Metamath Proof Explorer

Theorem tpnz

Description: An unordered triple containing a set is not empty. (Contributed by NM, 10-Apr-1994)

Ref Expression
Hypothesis tpnz.1 ⊢ A ∈ V
Assertion tpnz ⊢ A B C ≠ ∅

Proof

Step Hyp Ref Expression
1 tpnz.1 ⊢ A ∈ V
2 1 tpid1 ⊢ A ∈ A B C
3 2 ne0ii ⊢ A B C ≠ ∅