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

Theorem equncomi 3867
Description: Inference form of equncom 3866. equncomi 3867 was automatically derived from equncomiVD 39521 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 3866 . 2 (𝐴 = (𝐵𝐶) ↔ 𝐴 = (𝐶𝐵))
31, 2mpbi 220 1 𝐴 = (𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1596  cun 3678
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-v 3306  df-un 3685
This theorem is referenced by:  disjssun  4144  difprsn1  4438  unidmrn  5778  phplem1  8255  ackbij1lem14  9168  ltxrlt  10221  ruclem6  15084  ruclem7  15085  i1f1  23577  vtxdgoddnumeven  26580  subfacp1lem1  31389  lindsenlbs  33636  poimirlem6  33647  poimirlem7  33648  poimirlem16  33657  poimirlem17  33658  pwfi2f1o  38085  cnvrcl0  38351  iunrelexp0  38413  dfrtrcl4  38449  cotrclrcl  38453  dffrege76  38652  sucidALTVD  39522  sucidALT  39523
  Copyright terms: Public domain W3C validator