Theorem equncomi 3867

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

Syntax hints:   = wceq 1596   ∪ cun 3678

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-v 3306  df-un 3685

This theorem is referenced by:  disjssun  4144  difprsn1  4438  unidmrn  5778  phplem1  8255  ackbij1lem14  9168  ltxrlt  10221  ruclem6  15084  ruclem7  15085  i1f1  23577  vtxdgoddnumeven  26580  subfacp1lem1  31389  lindsenlbs  33636  poimirlem6  33647  poimirlem7  33648  poimirlem16  33657  poimirlem17  33658  pwfi2f1o  38085  cnvrcl0  38351  iunrelexp0  38413  dfrtrcl4  38449  cotrclrcl  38453  dffrege76  38652  sucidALTVD  39522  sucidALT  39523