Metamath Proof Explorer


Theorem in4

Description: Rearrangement of intersection of 4 classes. (Contributed by NM, 21-Apr-2001)

Ref Expression
Assertion in4 A B C D = A C B D

Proof

Step Hyp Ref Expression
1 in12 B C D = C B D
2 1 ineq2i A B C D = A C B D
3 inass A B C D = A B C D
4 inass A C B D = A C B D
5 2 3 4 3eqtr4i A B C D = A C B D