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

Theorem 19.29 1603
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 435 . . . 4  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
21alimi 1565 . . 3  |-  ( A. x ph  ->  A. x
( ps  ->  ( ph  /\  ps ) ) )
3 exim 1581 . . 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 419 1  |-  ( ( A. x ph  /\  E. x ps )  ->  E. x ( ph  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359   A.wal 1546   E.wex 1547
This theorem is referenced by:  19.29r  1604  19.29x  1606  equs4OLD  1952  equvini  2040  equviniOLD  2041  supsrlem  8942  1stccnp  17478  iscmet3  19199  isch3  22697  stoweidlem35  27651  bnj849  29002  equviniNEW7  29231  equs4NEW7  29237
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548
  Copyright terms: Public domain W3C validator