Theorem equncomi 4115

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

Syntax hints:   = wceq 1570   ∪ cun 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911

This theorem is referenced by:  disjssun  4429  difprsn1  4769  unidmrn  6282  djucomen  10162  ackbij1lem14  10216  ltxrlt  11281  ruclem6  16292  ruclem7  16293  i1f1  25830  vtxdgoddnumeven  29884  subfacp1lem1  35652  lindsenlbs  38247  poimirlem6  38258  poimirlem7  38259  poimirlem16  38268  poimirlem17  38269  pwfi2f1o  43806  cnvrcl0  44334  iunrelexp0  44411  dfrtrcl4  44447  cotrclrcl  44451  dffrege76  44648  sucidALTVD  45561  sucidALT  45562  usgrexmpl2edg  48777