Theorem equncomi 3721

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

Syntax hints:   = wceq 1475   ∪ cun 3538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545

This theorem is referenced by:  disjssun  3988  difprsn1  4271  unidmrn  5582  phplem1  8024  ackbij1lem14  8938  ltxrlt  9987  ruclem6  14803  ruclem7  14804  i1f1  23263  subfacp1lem1  30415  lindsenlbs  32574  poimirlem6  32585  poimirlem7  32586  poimirlem16  32595  poimirlem17  32596  pwfi2f1o  36684  cnvrcl0  36951  iunrelexp0  37013  dfrtrcl4  37049  cotrclrcl  37053  dffrege76  37253  sucidALTVD  38128  sucidALT  38129