MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  equncomi Structured version   Unicode version

Theorem equncomi 3591
Description: Inference form of equncom 3590. equncomi 3591 was automatically derived from equncomiVD 36713 using the tools program translatewithout_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
StepHypRef Expression
1 equncomi.1 . 2  |-  A  =  ( B  u.  C
)
2 equncom 3590 . 2  |-  ( A  =  ( B  u.  C )  <->  A  =  ( C  u.  B
) )
31, 2mpbi 210 1  |-  A  =  ( C  u.  B
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1407    u. cun 3414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382
This theorem depends on definitions:  df-bi 187  df-or 370  df-an 371  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-v 3063  df-un 3421
This theorem is referenced by:  disjssun  3829  difprsn1  4110  unidmrn  5356  phplem1  7736  ackbij1lem14  8647  ltxrlt  9688  ruclem6  14179  ruclem7  14180  i1f1  22391  subfacp1lem1  29489  pwfi2f1o  35419  pwfi2f1oOLD  35420  iunrelexp0  35694  dfrtrcl4  35730  cotrclrcl  35734  dffrege76  35933  sucidALTVD  36714  sucidALT  36715  usgfislem1  38086  usgfisALTlem1  38090
  Copyright terms: Public domain W3C validator