Metamath Proof Explorer


Theorem tpeq2

Description: Equality theorem for unordered triples. (Contributed by NM, 13-Sep-2011)

Ref Expression
Assertion tpeq2 A=BCAD=CBD

Proof

Step Hyp Ref Expression
1 preq2 A=BCA=CB
2 1 uneq1d A=BCAD=CBD
3 df-tp CAD=CAD
4 df-tp CBD=CBD
5 2 3 4 3eqtr4g A=BCAD=CBD