Theorem equncomi 4015

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

Syntax hints:   = wceq 1508   ∪ cun 3822

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-v 3412  df-un 3829

This theorem is referenced by:  disjssun  4295  difprsn1  4604  unidmrn  5966  phplem1  8491  djucomen  9400  ackbij1lem14  9452  ltxrlt  10510  ruclem6  15447  ruclem7  15448  i1f1  24010  vtxdgoddnumeven  27054  subfacp1lem1  32044  lindsenlbs  34361  poimirlem6  34372  poimirlem7  34373  poimirlem16  34382  poimirlem17  34383  pwfi2f1o  39126  cnvrcl0  39382  iunrelexp0  39444  dfrtrcl4  39480  cotrclrcl  39484  dffrege76  39682  sucidALTVD  40657  sucidALT  40658