Theorem equncomi 3759

Description: Inference form of equncom 3758. equncomi 3759 was automatically derived from equncomiVD 39105 using the tools program translate_without_overwriting.cmd and minimizing. (Contributed by Alan Sare, 18-Feb-2012.)

Hypothesis

Ref	Expression
equncomi.1	|- A = ( B u. C )

Assertion

Ref	Expression
equncomi	|- A = ( C u. B )

Proof of Theorem equncomi

Step	Hyp	Ref	Expression
1		equncomi.1	. 2 |- A = ( B u. C )
2		equncom 3758	. 2 |- ( A = ( B u. C ) <-> A = ( C u. B ) )
3	1, 2	mpbi 220	1 |- A = ( C u. B )

Syntax hints:   = wceq 1483   u. cun 3572

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579

This theorem is referenced by:  disjssun  4036  difprsn1  4330  unidmrn  5665  phplem1  8139  ackbij1lem14  9055  ltxrlt  10108  ruclem6  14964  ruclem7  14965  i1f1  23457  vtxdgoddnumeven  26449  subfacp1lem1  31161  lindsenlbs  33404  poimirlem6  33415  poimirlem7  33416  poimirlem16  33425  poimirlem17  33426  pwfi2f1o  37666  cnvrcl0  37932  iunrelexp0  37994  dfrtrcl4  38030  cotrclrcl  38034  dffrege76  38233  sucidALTVD  39106  sucidALT  39107