Theorem equncomi 4107

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

This proof depends on syntax axioms:   = wceq 1570   ∪ cun 3897

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904

This theorem is used by:  disjssun  4421  difprsn1  4763  unidmrn  6281  djucomen  10249  ackbij1lem14  10303  ltxrlt  11373  ruclem6  16396  ruclem7  16397  lindsenlbs  22150  i1f1  26004  vtxdgoddnumeven  30127  subfacp1lem1  35923  poimirlem6  38524  poimirlem7  38525  poimirlem16  38534  poimirlem17  38535  pwfi2f1o  44082  cnvrcl0  44610  iunrelexp0  44687  dfrtrcl4  44723  cotrclrcl  44727  dffrege76  44924  sucidALTVD  45837  sucidALT  45838  usgrexmpl2edg  49096