Theorem equncomi 4154

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

Hypothesis

Ref	Expression
equncomi.1	⊢ 𝐴 = (𝐵 ∪ 𝐶)

Assertion

Ref	Expression
equncomi	⊢ 𝐴 = (𝐶 ∪ 𝐵)

Proof of Theorem equncomi

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

Syntax hints:   = wceq 1539   ∪ cun 3945

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-un 3952

This theorem is referenced by:  disjssun  4466  difprsn1  4802  unidmrn  6277  phplem1OLD  9219  djucomen  10174  ackbij1lem14  10230  ltxrlt  11288  ruclem6  16182  ruclem7  16183  i1f1  25439  vtxdgoddnumeven  29077  subfacp1lem1  34468  lindsenlbs  36786  poimirlem6  36797  poimirlem7  36798  poimirlem16  36807  poimirlem17  36808  pwfi2f1o  42140  cnvrcl0  42678  iunrelexp0  42755  dfrtrcl4  42791  cotrclrcl  42795  dffrege76  42992  sucidALTVD  43933  sucidALT  43934