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

Theorem 19.41 1900
Description: Theorem 19.41 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 12-Jan-2018.)
Hypothesis
Ref Expression
19.41.1  |-  F/ x ps
Assertion
Ref Expression
19.41  |-  ( E. x ( ph  /\  ps )  <->  ( E. x ph  /\  ps ) )

Proof of Theorem 19.41
StepHypRef Expression
1 19.40 1619 . . 3  |-  ( E. x ( ph  /\  ps )  ->  ( E. x ph  /\  E. x ps ) )
2 19.41.1 . . . . 5  |-  F/ x ps
3219.9 1797 . . . 4  |-  ( E. x ps  <->  ps )
43anbi2i 676 . . 3  |-  ( ( E. x ph  /\  E. x ps )  <->  ( E. x ph  /\  ps )
)
51, 4sylib 189 . 2  |-  ( E. x ( ph  /\  ps )  ->  ( E. x ph  /\  ps ) )
6 pm3.21 436 . . . 4  |-  ( ps 
->  ( ph  ->  ( ph  /\  ps ) ) )
72, 6eximd 1786 . . 3  |-  ( ps 
->  ( E. x ph  ->  E. x ( ph  /\ 
ps ) ) )
87impcom 420 . 2  |-  ( ( E. x ph  /\  ps )  ->  E. x
( ph  /\  ps )
)
95, 8impbii 181 1  |-  ( E. x ( ph  /\  ps )  <->  ( E. x ph  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359   E.wex 1550   F/wnf 1553
This theorem is referenced by:  19.42  1902  exan  1903  19.41v  1924  eean  1936  eeeanv  1938  r19.41  2860  eliunxp  5012  dfopab2  6401  dfoprab3s  6402  xpcomco  7198  2sb5nd  28647  2sb5ndVD  29022  2sb5ndALT  29044  bnj605  29278  bnj607  29287  eeanOLD7  29702
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554
  Copyright terms: Public domain W3C validator