Metamath Proof Explorer


Theorem brtpid3

Description: A binary relation involving unordered triples. (Contributed by Scott Fenton, 7-Jun-2016)

Ref Expression
Assertion brtpid3 A C D A B B

Proof

Step Hyp Ref Expression
1 opex A B V
2 1 tpid3 A B C D A B
3 df-br A C D A B B A B C D A B
4 2 3 mpbir A C D A B B