Theorem equncomi 4089

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

Syntax hints:   = wceq 1539   ∪ cun 3885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-un 3892

This theorem is referenced by:  disjssun  4401  difprsn1  4733  unidmrn  6182  phplem1OLD  9000  djucomen  9933  ackbij1lem14  9989  ltxrlt  11045  ruclem6  15944  ruclem7  15945  i1f1  24854  vtxdgoddnumeven  27920  subfacp1lem1  33141  lindsenlbs  35772  poimirlem6  35783  poimirlem7  35784  poimirlem16  35793  poimirlem17  35794  pwfi2f1o  40921  cnvrcl0  41233  iunrelexp0  41310  dfrtrcl4  41346  cotrclrcl  41350  dffrege76  41547  sucidALTVD  42490  sucidALT  42491