Metamath Proof Explorer


Theorem in12

Description: A rearrangement of intersection. (Contributed by NM, 21-Apr-2001)

Ref Expression
Assertion in12 A B C = B A C

Proof

Step Hyp Ref Expression
1 incom A B = B A
2 1 ineq1i A B C = B A C
3 inass A B C = A B C
4 inass B A C = B A C
5 2 3 4 3eqtr3i A B C = B A C