Theorem equncomi

Description: Inference form of equncom . equncomi was automatically derived from equncomiVD using the tools program translate__without__overwriting.cmd and minimizing. (Contributed by Alan Sare, 18-Feb-2012)

	Ref	Expression
Hypothesis	equncomi.1	|- A = ( B u. C )
Assertion	equncomi	|- A = ( C u. B )

Proof

Step	Hyp	Ref	Expression
1		equncomi.1	|- A = ( B u. C )
2		equncom	|- ( A = ( B u. C ) <-> A = ( C u. B ) )
3	1 2	mpbi	|- A = ( C u. B )