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

Theorem equncomi 3890
Description: Inference form of equncom 3889. equncomi 3890 was automatically derived from equncomiVD 39573 using the tools program translatewithout_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 3889 . 2 (𝐴 = (𝐵𝐶) ↔ 𝐴 = (𝐶𝐵))
31, 2mpbi 220 1 𝐴 = (𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1620  cun 3701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-v 3330  df-un 3708
This theorem is referenced by:  disjssun  4168  difprsn1  4463  unidmrn  5814  phplem1  8292  ackbij1lem14  9218  ltxrlt  10271  ruclem6  15134  ruclem7  15135  i1f1  23627  vtxdgoddnumeven  26630  subfacp1lem1  31439  lindsenlbs  33686  poimirlem6  33697  poimirlem7  33698  poimirlem16  33707  poimirlem17  33708  pwfi2f1o  38137  cnvrcl0  38403  iunrelexp0  38465  dfrtrcl4  38501  cotrclrcl  38505  dffrege76  38704  sucidALTVD  39574  sucidALT  39575
  Copyright terms: Public domain W3C validator