This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∪ C
Assertion equncomi ⊢ A = C ∪ B

Proof

Step Hyp Ref Expression
1 equncomi.1 ⊢ A = B ∪ C
2 equncom ⊢ A = B ∪ C ↔ A = C ∪ B
3 1 2 mpbi ⊢ A = C ∪ B