Theorem equncomi 4162

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

This proof depends on syntax axioms:   = wceq 1570   ∪ cun 4152

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-un 4154

This theorem is used by:  disjssun  4424  difprsn1  4765  unidmrn  6306  djucomen  10295  ackbij1lem14  10349  ltxrlt  11419  ruclem6  16447  ruclem7  16448  lindsenlbs  22212  i1f1  26066  vtxdgoddnumeven  30191  subfacp1lem1  36152  poimirlem6  38812  poimirlem7  38813  poimirlem16  38822  poimirlem17  38823  pwfi2f1o  44364  cnvrcl0  44886  iunrelexp0  44963  dfrtrcl4  44999  cotrclrcl  45003  dffrege76  45200  sucidALTVD  46112  sucidALT  46113  usgrexmpl2edg  49400