Theorem equncomi 4142

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

Syntax hints:   = wceq 1539   ∪ cun 3931

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-v 3466  df-un 3938

This theorem is referenced by:  disjssun  4450  difprsn1  4782  unidmrn  6281  phplem1OLD  9237  djucomen  10201  ackbij1lem14  10255  ltxrlt  11314  ruclem6  16254  ruclem7  16255  i1f1  25680  vtxdgoddnumeven  29518  subfacp1lem1  35125  lindsenlbs  37563  poimirlem6  37574  poimirlem7  37575  poimirlem16  37584  poimirlem17  37585  pwfi2f1o  43053  cnvrcl0  43583  iunrelexp0  43660  dfrtrcl4  43696  cotrclrcl  43700  dffrege76  43897  sucidALTVD  44835  sucidALT  44836  usgrexmpl2edg  47934