Theorem equncomi 3890

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

Syntax hints:   = wceq 1620   ∪ cun 3701

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-v 3330  df-un 3708

This theorem is referenced by:  disjssun  4168  difprsn1  4463  unidmrn  5814  phplem1  8292  ackbij1lem14  9218  ltxrlt  10271  ruclem6  15134  ruclem7  15135  i1f1  23627  vtxdgoddnumeven  26630  subfacp1lem1  31439  lindsenlbs  33686  poimirlem6  33697  poimirlem7  33698  poimirlem16  33707  poimirlem17  33708  pwfi2f1o  38137  cnvrcl0  38403  iunrelexp0  38465  dfrtrcl4  38501  cotrclrcl  38505  dffrege76  38704  sucidALTVD  39574  sucidALT  39575