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

Theorem exbi 1579
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 180 . . . 4  |-  ( (
ph 
<->  ps )  ->  ( ph  ->  ps ) )
21alimi 1546 . . 3  |-  ( A. x ( ph  <->  ps )  ->  A. x ( ph  ->  ps ) )
3 exim 1573 . . 3  |-  ( A. x ( ph  ->  ps )  ->  ( E. x ph  ->  E. x ps ) )
42, 3syl 17 . 2  |-  ( A. x ( ph  <->  ps )  ->  ( E. x ph  ->  E. x ps )
)
5 bi2 191 . . . 4  |-  ( (
ph 
<->  ps )  ->  ( ps  ->  ph ) )
65alimi 1546 . . 3  |-  ( A. x ( ph  <->  ps )  ->  A. x ( ps 
->  ph ) )
7 exim 1573 . . 3  |-  ( A. x ( ps  ->  ph )  ->  ( E. x ps  ->  E. x ph ) )
86, 7syl 17 . 2  |-  ( A. x ( ph  <->  ps )  ->  ( E. x ps 
->  E. x ph )
)
94, 8impbid 185 1  |-  ( A. x ( ph  <->  ps )  ->  ( E. x ph  <->  E. x ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178   A.wal 1532   E.wex 1537
This theorem is referenced by:  exbii  1580  exbidh  1590  exintrbi  1615  19.19  1769  2exbi  26744  rexbidar  26816  onfrALTlem5VD  27448  onfrALTlem1VD  27453  csbxpgVD  27457  csbrngVD  27459  csbunigVD  27461  e2ebindVD  27475  e2ebindALT  27493  bnj956  27594
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536
This theorem depends on definitions:  df-bi 179  df-ex 1538
  Copyright terms: Public domain W3C validator