Theorem equncomi 4171

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

Syntax hints:   = wceq 1538   ∪ cun 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1541  df-ex 1778  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-un 3969

This theorem is referenced by:  disjssun  4475  difprsn1  4806  unidmrn  6304  phplem1OLD  9258  djucomen  10222  ackbij1lem14  10276  ltxrlt  11335  ruclem6  16274  ruclem7  16275  i1f1  25747  vtxdgoddnumeven  29594  subfacp1lem1  35176  lindsenlbs  37614  poimirlem6  37625  poimirlem7  37626  poimirlem16  37635  poimirlem17  37636  pwfi2f1o  43099  cnvrcl0  43629  iunrelexp0  43706  dfrtrcl4  43742  cotrclrcl  43746  dffrege76  43943  sucidALTVD  44881  sucidALT  44882  usgrexmpl2edg  47937