Theorem equncomi 4114

Description: Inference form of equncom 4113. equncomi 4114 was automatically derived from equncomiVD 45221 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 230	1 ⊢ 𝐴 = (𝐶 ∪ 𝐵)

Syntax hints:   = wceq 1542   ∪ cun 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908

This theorem is referenced by:  disjssun  4422  difprsn1  4758  unidmrn  6245  djucomen  10100  ackbij1lem14  10154  ltxrlt  11215  ruclem6  16172  ruclem7  16173  i1f1  25659  vtxdgoddnumeven  29639  subfacp1lem1  35392  lindsenlbs  37863  poimirlem6  37874  poimirlem7  37875  poimirlem16  37884  poimirlem17  37885  pwfi2f1o  43450  cnvrcl0  43978  iunrelexp0  44055  dfrtrcl4  44091  cotrclrcl  44095  dffrege76  44292  sucidALTVD  45222  sucidALT  45223  usgrexmpl2edg  48386