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

Metamath Proof Explorer

Theorem disjtpsn

Description: The disjoint intersection of an unordered triple and a singleton. (Contributed by AV, 14-Nov-2021)

Ref Expression
Assertion disjtpsn ⊢ A ≠ D ∧ B ≠ D ∧ C ≠ D → A B C ∩ D = ∅

Proof

Step Hyp Ref Expression
1 df-tp ⊢ A B C = A B ∪ C
2 1 ineq1i ⊢ A B C ∩ D = A B ∪ C ∩ D
3 disjprsn ⊢ A ≠ D ∧ B ≠ D → A B ∩ D = ∅
4 3 3adant3 ⊢ A ≠ D ∧ B ≠ D ∧ C ≠ D → A B ∩ D = ∅
5 disjsn2 ⊢ C ≠ D → C ∩ D = ∅
6 5 3ad2ant3 ⊢ A ≠ D ∧ B ≠ D ∧ C ≠ D → C ∩ D = ∅
7 4 6 jca ⊢ A ≠ D ∧ B ≠ D ∧ C ≠ D → A B ∩ D = ∅ ∧ C ∩ D = ∅
8 undisj1 ⊢ A B ∩ D = ∅ ∧ C ∩ D = ∅ ↔ A B ∪ C ∩ D = ∅
9 7 8 sylib ⊢ A ≠ D ∧ B ≠ D ∧ C ≠ D → A B ∪ C ∩ D = ∅
10 2 9 eqtrid ⊢ A ≠ D ∧ B ≠ D ∧ C ≠ D → A B C ∩ D = ∅