Metamath Proof Explorer


Theorem tpeq2d

Description: Equality theorem for unordered triples. (Contributed by NM, 22-Jun-2014)

Ref Expression
Hypothesis tpeq1d.1 φA=B
Assertion tpeq2d φCAD=CBD

Proof

Step Hyp Ref Expression
1 tpeq1d.1 φA=B
2 tpeq2 A=BCAD=CBD
3 1 2 syl φCAD=CBD