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

Theorem exbi 1568
Description: Theorem 19.18 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
exbi  |-  ( A. x ( ph  <->  ps )  ->  ( E. x ph  <->  E. x ps ) )

Proof of Theorem exbi
StepHypRef Expression
1 bi1 178 . . . 4  |-  ( (
ph 
<->  ps )  ->  ( ph  ->  ps ) )
21alimi 1546 . . 3  |-  ( A. x ( ph  <->  ps )  ->  A. x ( ph  ->  ps ) )
3 exim 1562 . . 3  |-  ( A. x ( ph  ->  ps )  ->  ( E. x ph  ->  E. x ps ) )
42, 3syl 15 . 2  |-  ( A. x ( ph  <->  ps )  ->  ( E. x ph  ->  E. x ps )
)
5 bi2 189 . . . 4  |-  ( (
ph 
<->  ps )  ->  ( ps  ->  ph ) )
65alimi 1546 . . 3  |-  ( A. x ( ph  <->  ps )  ->  A. x ( ps 
->  ph ) )
7 exim 1562 . . 3  |-  ( A. x ( ps  ->  ph )  ->  ( E. x ps  ->  E. x ph ) )
86, 7syl 15 . 2  |-  ( A. x ( ph  <->  ps )  ->  ( E. x ps 
->  E. x ph )
)
94, 8impbid 183 1  |-  ( A. x ( ph  <->  ps )  ->  ( E. x ph  <->  E. x ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wal 1527   E.wex 1528
This theorem is referenced by:  exbii  1569  exbidh  1578  exintrbi  1600  19.19  1789  2exbi  27578  rexbidar  27649  onfrALTlem5VD  28661  onfrALTlem1VD  28666  csbxpgVD  28670  csbrngVD  28672  csbunigVD  28674  e2ebindVD  28688  e2ebindALT  28706  bnj956  28808
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544
This theorem depends on definitions:  df-bi 177  df-ex 1529
  Copyright terms: Public domain W3C validator