Theorem ineqcomi

Description: Disjointness inference (when C = (/) ), inference form of ineqcom . (Contributed by Peter Mazsa, 26-Mar-2017)

	Ref	Expression
Hypothesis	ineqcomi.1	|- ( A i^i B ) = C
Assertion	ineqcomi	|- ( B i^i A ) = C

Proof

Step	Hyp	Ref	Expression
1		ineqcomi.1	|- ( A i^i B ) = C
2		ineqcom	|- ( ( A i^i B ) = C <-> ( B i^i A ) = C )
3	1 2	mpbi	|- ( B i^i A ) = C