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

Theorem equncomi 4085
Description: Inference form of equncom 4084. equncomi 4085 was automatically derived from equncomiVD 41568 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
StepHypRef Expression
1 equncomi.1 . 2 𝐴 = (𝐵𝐶)
2 equncom 4084 . 2 (𝐴 = (𝐵𝐶) ↔ 𝐴 = (𝐶𝐵))
31, 2mpbi 233 1 𝐴 = (𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  cun 3882
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-un 3889
This theorem is referenced by:  disjssun  4378  difprsn1  4696  unidmrn  6102  phplem1  8684  djucomen  9592  ackbij1lem14  9648  ltxrlt  10704  ruclem6  15584  ruclem7  15585  i1f1  24298  vtxdgoddnumeven  27347  subfacp1lem1  32540  lindsenlbs  35051  poimirlem6  35062  poimirlem7  35063  poimirlem16  35072  poimirlem17  35073  pwfi2f1o  40033  cnvrcl0  40318  iunrelexp0  40396  dfrtrcl4  40432  cotrclrcl  40436  dffrege76  40633  sucidALTVD  41569  sucidALT  41570
  Copyright terms: Public domain W3C validator