Theorem equncomi 4111

Description: Inference form of equncom 4110. equncomi 4111 was automatically derived from equncomiVD 45405 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 4110	. 2 ⊢ (𝐴 = (𝐵 ∪ 𝐶) ↔ 𝐴 = (𝐶 ∪ 𝐵))
3	1, 2	mpbi 232	1 ⊢ 𝐴 = (𝐶 ∪ 𝐵)

Syntax hints:   = wceq 1559   ∪ cun 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3907

This theorem is referenced by:  disjssun  4419  difprsn1  4757  unidmrn  6261  djucomen  10128  ackbij1lem14  10182  ltxrlt  11247  ruclem6  16258  ruclem7  16259  i1f1  25740  vtxdgoddnumeven  29711  subfacp1lem1  35490  lindsenlbs  38075  poimirlem6  38086  poimirlem7  38087  poimirlem16  38096  poimirlem17  38097  pwfi2f1o  43634  cnvrcl0  44162  iunrelexp0  44239  dfrtrcl4  44275  cotrclrcl  44279  dffrege76  44476  sucidALTVD  45406  sucidALT  45407  usgrexmpl2edg  48612