Theorem equncomi 4120

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

Syntax hints:   = wceq 1541   ∪ cun 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-un 3918

This theorem is referenced by:  disjssun  4432  difprsn1  4765  unidmrn  6236  phplem1OLD  9168  djucomen  10122  ackbij1lem14  10178  ltxrlt  11234  ruclem6  16128  ruclem7  16129  i1f1  25091  vtxdgoddnumeven  28564  subfacp1lem1  33860  lindsenlbs  36146  poimirlem6  36157  poimirlem7  36158  poimirlem16  36167  poimirlem17  36168  pwfi2f1o  41481  cnvrcl0  42019  iunrelexp0  42096  dfrtrcl4  42132  cotrclrcl  42136  dffrege76  42333  sucidALTVD  43274  sucidALT  43275