Metamath Proof Explorer


Theorem iniin2

Description: Indexed intersection of intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Assertion iniin2 ABxAC=xABC

Proof

Step Hyp Ref Expression
1 iinin2 AxABC=BxAC
2 1 eqcomd ABxAC=xABC