Theorem equncomi 4107

Description: Inference form of equncom 4106. equncomi 4107 was automatically derived from equncomiVD 45691 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 2732

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 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904

This theorem is used by:  disjssun  4421  difprsn1  4763  unidmrn  6277  djucomen  10180  ackbij1lem14  10234  ltxrlt  11304  ruclem6  16323  ruclem7  16324  lindsenlbs  22064  i1f1  25918  vtxdgoddnumeven  30013  subfacp1lem1  35758  poimirlem6  38375  poimirlem7  38376  poimirlem16  38385  poimirlem17  38386  pwfi2f1o  43937  cnvrcl0  44465  iunrelexp0  44542  dfrtrcl4  44578  cotrclrcl  44582  dffrege76  44779  sucidALTVD  45692  sucidALT  45693  usgrexmpl2edg  48945