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 AV
Assertion tpnz ABC

Proof

Step Hyp Ref Expression
1 tpnz.1 AV
2 1 tpid1 AABC
3 2 ne0ii ABC