Theorem equncomi 4112

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

Syntax hints:   = wceq 1541   ∪ cun 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906

This theorem is referenced by:  disjssun  4420  difprsn1  4756  unidmrn  6237  djucomen  10088  ackbij1lem14  10142  ltxrlt  11203  ruclem6  16160  ruclem7  16161  i1f1  25647  vtxdgoddnumeven  29627  subfacp1lem1  35373  lindsenlbs  37816  poimirlem6  37827  poimirlem7  37828  poimirlem16  37837  poimirlem17  37838  pwfi2f1o  43338  cnvrcl0  43866  iunrelexp0  43943  dfrtrcl4  43979  cotrclrcl  43983  dffrege76  44180  sucidALTVD  45110  sucidALT  45111  usgrexmpl2edg  48275