MPE Home 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  |-  ( ( A. x ph  /\  E. x ps )  ->  E. x ( ph  /\  ps ) )

Proof of Theorem 19.29
StepHypRef Expression
1 pm3.2 436 . . . 4  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
21alimi 1569 . . 3  |-  ( A. x ph  ->  A. x
( ps  ->  ( ph  /\  ps ) ) )
3 exim 1585 . . 3  |-  ( A. x ( ps  ->  (
ph  /\  ps )
)  ->  ( E. x ps  ->  E. x
( ph  /\  ps )
) )
42, 3syl 16 . 2  |-  ( A. x ph  ->  ( E. x ps  ->  E. x
( ph  /\  ps )
) )
54imp 420 1  |-  ( ( A. x ph  /\  E. x ps )  ->  E. x ( ph  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360   A.wal 1550   E.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