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

Theorem equncomi 3649
 Description: Inference form of equncom 3648. equncomi 3649 was automatically derived from equncomiVD 33669 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 3648 . 2
31, 2mpbi 208 1
 Colors of variables: wff setvar class Syntax hints:  =wceq 1395  u.cun 3473 This theorem is referenced by:  disjssun  3884  difprsn1  4166  unidmrn  5542  phplem1  7716  ackbij1lem14  8634  ltxrlt  9676  ruclem6  13968  ruclem7  13969  i1f1  22097  subfacp1lem1  28623  pwfi2f1o  31044  usgfislem1  32444  usgfisALTlem1  32448  sucidALTVD  33670  sucidALT  33671 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3480
 Copyright terms: Public domain W3C validator