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

Theorem 19.35 1610
Description: Theorem 19.35 of [Margaris] p. 90. This theorem is useful for moving an implication (in the form of the right-hand side) into the scope of a single existential quantifier. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 27-Jun-2014.)
Assertion
Ref Expression
19.35  |-  ( E. x ( ph  ->  ps )  <->  ( A. x ph  ->  E. x ps )
)

Proof of Theorem 19.35
StepHypRef Expression
1 19.26 1603 . . . 4  |-  ( A. x ( ph  /\  -.  ps )  <->  ( A. x ph  /\  A. x  -.  ps ) )
2 annim 415 . . . . 5  |-  ( (
ph  /\  -.  ps )  <->  -.  ( ph  ->  ps ) )
32albii 1575 . . . 4  |-  ( A. x ( ph  /\  -.  ps )  <->  A. x  -.  ( ph  ->  ps ) )
4 alnex 1552 . . . . 5  |-  ( A. x  -.  ps  <->  -.  E. x ps )
54anbi2i 676 . . . 4  |-  ( ( A. x ph  /\  A. x  -.  ps )  <->  ( A. x ph  /\  -.  E. x ps )
)
61, 3, 53bitr3i 267 . . 3  |-  ( A. x  -.  ( ph  ->  ps )  <->  ( A. x ph  /\  -.  E. x ps ) )
7 alnex 1552 . . 3  |-  ( A. x  -.  ( ph  ->  ps )  <->  -.  E. x
( ph  ->  ps )
)
8 annim 415 . . 3  |-  ( ( A. x ph  /\  -.  E. x ps )  <->  -.  ( A. x ph  ->  E. x ps )
)
96, 7, 83bitr3i 267 . 2  |-  ( -. 
E. x ( ph  ->  ps )  <->  -.  ( A. x ph  ->  E. x ps ) )
109con4bii 289 1  |-  ( E. x ( ph  ->  ps )  <->  ( A. x ph  ->  E. x ps )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    /\ wa 359   A.wal 1549   E.wex 1550
This theorem is referenced by:  19.35i  1611  19.35ri  1612  19.25  1613  19.43  1615  speimfw  1655  19.39  1673  19.24  1674  19.36  1892  19.37  1894  spimt  1955  sbequiOLD  2114  grothprim  8709  sbequiNEW7  29579
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