Theorem equncomi 4114

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

Syntax hints:   = wceq 1542   ∪ cun 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908

This theorem is referenced by:  disjssun  4422  difprsn1  4758  unidmrn  6247  djucomen  10102  ackbij1lem14  10156  ltxrlt  11217  ruclem6  16174  ruclem7  16175  i1f1  25664  vtxdgoddnumeven  29645  subfacp1lem1  35401  lindsenlbs  37895  poimirlem6  37906  poimirlem7  37907  poimirlem16  37916  poimirlem17  37917  pwfi2f1o  43482  cnvrcl0  44010  iunrelexp0  44087  dfrtrcl4  44123  cotrclrcl  44127  dffrege76  44324  sucidALTVD  45254  sucidALT  45255  usgrexmpl2edg  48418