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

Theorem equncomi 4015
 Description: Inference form of equncom 4014. equncomi 4015 was automatically derived from equncomiVD 40656 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 4014 . 2 (𝐴 = (𝐵𝐶) ↔ 𝐴 = (𝐶𝐵))
31, 2mpbi 222 1 𝐴 = (𝐶𝐵)
 Colors of variables: wff setvar class Syntax hints:   = wceq 1508   ∪ cun 3822 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2745 This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-v 3412  df-un 3829 This theorem is referenced by:  disjssun  4295  difprsn1  4604  unidmrn  5966  phplem1  8491  djucomen  9400  ackbij1lem14  9452  ltxrlt  10510  ruclem6  15447  ruclem7  15448  i1f1  24010  vtxdgoddnumeven  27054  subfacp1lem1  32044  lindsenlbs  34361  poimirlem6  34372  poimirlem7  34373  poimirlem16  34382  poimirlem17  34383  pwfi2f1o  39126  cnvrcl0  39382  iunrelexp0  39444  dfrtrcl4  39480  cotrclrcl  39484  dffrege76  39682  sucidALTVD  40657  sucidALT  40658
 Copyright terms: Public domain W3C validator