Theorem equncomi 4183

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

Syntax hints:   = wceq 1537   ∪ cun 3974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981

This theorem is referenced by:  disjssun  4491  difprsn1  4825  unidmrn  6310  phplem1OLD  9280  djucomen  10247  ackbij1lem14  10301  ltxrlt  11360  ruclem6  16283  ruclem7  16284  i1f1  25744  vtxdgoddnumeven  29589  subfacp1lem1  35147  lindsenlbs  37575  poimirlem6  37586  poimirlem7  37587  poimirlem16  37596  poimirlem17  37597  pwfi2f1o  43053  cnvrcl0  43587  iunrelexp0  43664  dfrtrcl4  43700  cotrclrcl  43704  dffrege76  43901  sucidALTVD  44841  sucidALT  44842  usgrexmpl2edg  47844