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

Theorem equncomi 4154
Description: Inference form of equncom 4153. equncomi 4154 was automatically derived from equncomiVD 43932 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 4153 . 2 (𝐴 = (𝐵𝐶) ↔ 𝐴 = (𝐶𝐵))
31, 2mpbi 229 1 𝐴 = (𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1539  cun 3945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-un 3952
This theorem is referenced by:  disjssun  4466  difprsn1  4802  unidmrn  6277  phplem1OLD  9219  djucomen  10174  ackbij1lem14  10230  ltxrlt  11288  ruclem6  16182  ruclem7  16183  i1f1  25439  vtxdgoddnumeven  29077  subfacp1lem1  34468  lindsenlbs  36786  poimirlem6  36797  poimirlem7  36798  poimirlem16  36807  poimirlem17  36808  pwfi2f1o  42140  cnvrcl0  42678  iunrelexp0  42755  dfrtrcl4  42791  cotrclrcl  42795  dffrege76  42992  sucidALTVD  43933  sucidALT  43934
  Copyright terms: Public domain W3C validator