Theorem equncomi 4085

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

Syntax hints:   = wceq 1539   ∪ cun 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888

This theorem is referenced by:  disjssun  4398  difprsn1  4730  unidmrn  6171  phplem1  8892  djucomen  9864  ackbij1lem14  9920  ltxrlt  10976  ruclem6  15872  ruclem7  15873  i1f1  24759  vtxdgoddnumeven  27823  subfacp1lem1  33041  lindsenlbs  35699  poimirlem6  35710  poimirlem7  35711  poimirlem16  35720  poimirlem17  35721  pwfi2f1o  40837  cnvrcl0  41122  iunrelexp0  41199  dfrtrcl4  41235  cotrclrcl  41239  dffrege76  41436  sucidALTVD  42379  sucidALT  42380