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

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 ⊢ φ → A ∈ V
Assertion tpnzd ⊢ φ → A B C ≠ ∅

Proof

Step Hyp Ref Expression
1 tpnzd.1 ⊢ φ → A ∈ V
2 tpid1g ⊢ A ∈ V → A ∈ A B C
3 ne0i ⊢ A ∈ A B C → A B C ≠ ∅
4 1 2 3 3syl ⊢ φ → A B C ≠ ∅