Theorem equncomi 4122

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

Syntax hints:   = wceq 1567   ∪ cun 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918

This theorem is referenced by:  disjssun  4431  difprsn1  4769  unidmrn  6277  djucomen  10157  ackbij1lem14  10211  ltxrlt  11276  ruclem6  16287  ruclem7  16288  i1f1  25814  vtxdgoddnumeven  29840  subfacp1lem1  35566  lindsenlbs  38149  poimirlem6  38160  poimirlem7  38161  poimirlem16  38170  poimirlem17  38171  pwfi2f1o  43708  cnvrcl0  44236  iunrelexp0  44313  dfrtrcl4  44349  cotrclrcl  44353  dffrege76  44550  sucidALTVD  45463  sucidALT  45464  usgrexmpl2edg  48676