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	⊢ 𝐴 = ( 𝐵 ∪ 𝐶 )
Assertion	equncomi	⊢ 𝐴 = ( 𝐶 ∪ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		equncomi.1	⊢ 𝐴 = ( 𝐵 ∪ 𝐶 )
2		equncom	⊢ ( 𝐴 = ( 𝐵 ∪ 𝐶 ) ↔ 𝐴 = ( 𝐶 ∪ 𝐵 ) )
3	1 2	mpbi	⊢ 𝐴 = ( 𝐶 ∪ 𝐵 )