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

Theorem 19.29 1607
 Description: Theorem 19.29 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.)
Assertion
Ref Expression
19.29

Proof of Theorem 19.29
StepHypRef Expression
1 pm3.2 436 . . . 4
21alimi 1569 . . 3
3 exim 1585 . . 3
42, 3syl 16 . 2
54imp 420 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 360  wal 1550  wex 1551 This theorem is referenced by:  19.29r  1608  19.29x  1610  equs4OLD  1999  equvini  2084  equviniOLD  2085  supsrlem  8988  1stccnp  17527  iscmet3  19248  isch3  22746  stoweidlem35  27762  bnj849  29358  equviniNEW7  29589  equs4NEW7  29595 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567 This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552
 Copyright terms: Public domain W3C validator