Theorem equncomi 4140

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

Syntax hints:   = wceq 1540   ∪ cun 3929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-un 3936

This theorem is referenced by:  disjssun  4448  difprsn1  4781  unidmrn  6273  phplem1OLD  9233  djucomen  10197  ackbij1lem14  10251  ltxrlt  11310  ruclem6  16258  ruclem7  16259  i1f1  25648  vtxdgoddnumeven  29538  subfacp1lem1  35206  lindsenlbs  37644  poimirlem6  37655  poimirlem7  37656  poimirlem16  37665  poimirlem17  37666  pwfi2f1o  43095  cnvrcl0  43624  iunrelexp0  43701  dfrtrcl4  43737  cotrclrcl  43741  dffrege76  43938  sucidALTVD  44869  sucidALT  44870  usgrexmpl2edg  48013