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

Theorem 19.29r 1607
Description: Variation of Theorem 19.29 of [Margaris] p. 90. (Contributed by NM, 18-Aug-1993.)
Assertion
Ref Expression
19.29r  |-  ( ( E. x ph  /\  A. x ps )  ->  E. x ( ph  /\  ps ) )

Proof of Theorem 19.29r
StepHypRef Expression
1 19.29 1606 . . 3  |-  ( ( A. x ps  /\  E. x ph )  ->  E. x ( ps  /\  ph ) )
21ancoms 440 . 2  |-  ( ( E. x ph  /\  A. x ps )  ->  E. x ( ps  /\  ph ) )
3 exancom 1596 . 2  |-  ( E. x ( ph  /\  ps )  <->  E. x ( ps 
/\  ph ) )
42, 3sylibr 204 1  |-  ( ( E. x ph  /\  A. x ps )  ->  E. x ( ph  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359   A.wal 1549   E.wex 1550
This theorem is referenced by:  19.29r2  1608  19.29x  1609  exanOLD  1904  equvini  2083  equviniOLD  2084  eu2  2306  intab  4080  imadif  5528  kmlem6  8035  2ndcdisj  17519  fmcncfil  24317  bnj907  29336  equviniNEW7  29527
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551
  Copyright terms: Public domain W3C validator