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

Theorem equncomi 4151
Description: Inference form of equncom 4150. equncomi 4151 was automatically derived from equncomiVD 43401 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 4150 . 2 (𝐴 = (𝐵𝐶) ↔ 𝐴 = (𝐶𝐵))
31, 2mpbi 229 1 𝐴 = (𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1541  cun 3942
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-un 3949
This theorem is referenced by:  disjssun  4463  difprsn1  4796  unidmrn  6267  phplem1OLD  9200  djucomen  10154  ackbij1lem14  10210  ltxrlt  11266  ruclem6  16160  ruclem7  16161  i1f1  25136  vtxdgoddnumeven  28675  subfacp1lem1  34001  lindsenlbs  36287  poimirlem6  36298  poimirlem7  36299  poimirlem16  36308  poimirlem17  36309  pwfi2f1o  41609  cnvrcl0  42147  iunrelexp0  42224  dfrtrcl4  42260  cotrclrcl  42264  dffrege76  42461  sucidALTVD  43402  sucidALT  43403
  Copyright terms: Public domain W3C validator