Theorem equncomi 4110

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

Syntax hints:   = wceq 1541   ∪ cun 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3907

This theorem is referenced by:  disjssun  4418  difprsn1  4752  unidmrn  6226  djucomen  10069  ackbij1lem14  10123  ltxrlt  11183  ruclem6  16144  ruclem7  16145  i1f1  25619  vtxdgoddnumeven  29533  subfacp1lem1  35221  lindsenlbs  37661  poimirlem6  37672  poimirlem7  37673  poimirlem16  37682  poimirlem17  37683  pwfi2f1o  43135  cnvrcl0  43664  iunrelexp0  43741  dfrtrcl4  43777  cotrclrcl  43781  dffrege76  43978  sucidALTVD  44908  sucidALT  44909  usgrexmpl2edg  48066