Theorem equncomi 4114

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911

This theorem is used by:  disjssun  4428  difprsn1  4770  unidmrn  6284  djucomen  10173  ackbij1lem14  10227  ltxrlt  11291  ruclem6  16309  ruclem7  16310  i1f1  25880  vtxdgoddnumeven  29937  subfacp1lem1  35684  lindsenlbs  38299  poimirlem6  38310  poimirlem7  38311  poimirlem16  38320  poimirlem17  38321  pwfi2f1o  43856  cnvrcl0  44384  iunrelexp0  44461  dfrtrcl4  44497  cotrclrcl  44501  dffrege76  44698  sucidALTVD  45611  sucidALT  45612  usgrexmpl2edg  48827