Theorem equncomi 4158

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

This proof depends on syntax axioms:   = wceq 1569   ∪ cun 4148

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 4150

This theorem is used by:  disjssun  4420  difprsn1  4759  unidmrn  6284  djucomen  10261  ackbij1lem14  10315  ltxrlt  11385  ruclem6  16410  ruclem7  16411  lindsenlbs  22164  i1f1  26018  vtxdgoddnumeven  30141  subfacp1lem1  36032  poimirlem6  38651  poimirlem7  38652  poimirlem16  38661  poimirlem17  38662  pwfi2f1o  44205  cnvrcl0  44732  iunrelexp0  44809  dfrtrcl4  44845  cotrclrcl  44849  dffrege76  45046  sucidALTVD  45959  sucidALT  45960  usgrexmpl2edg  49234