Theorem equncomi 4055

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

Syntax hints:   = wceq 1543   ∪ cun 3851

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-un 3858

This theorem is referenced by:  disjssun  4368  difprsn1  4699  unidmrn  6122  phplem1  8803  djucomen  9756  ackbij1lem14  9812  ltxrlt  10868  ruclem6  15759  ruclem7  15760  i1f1  24541  vtxdgoddnumeven  27595  subfacp1lem1  32808  lindsenlbs  35458  poimirlem6  35469  poimirlem7  35470  poimirlem16  35479  poimirlem17  35480  pwfi2f1o  40565  cnvrcl0  40850  iunrelexp0  40928  dfrtrcl4  40964  cotrclrcl  40968  dffrege76  41165  sucidALTVD  42104  sucidALT  42105