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

Theorem exbi 1588
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 179 . . . 4  |-  ( (
ph 
<->  ps )  ->  ( ph  ->  ps ) )
21alimi 1565 . . 3  |-  ( A. x ( ph  <->  ps )  ->  A. x ( ph  ->  ps ) )
3 exim 1581 . . 3  |-  ( A. x ( ph  ->  ps )  ->  ( E. x ph  ->  E. x ps ) )
42, 3syl 16 . 2  |-  ( A. x ( ph  <->  ps )  ->  ( E. x ph  ->  E. x ps )
)
5 bi2 190 . . . 4  |-  ( (
ph 
<->  ps )  ->  ( ps  ->  ph ) )
65alimi 1565 . . 3  |-  ( A. x ( ph  <->  ps )  ->  A. x ( ps 
->  ph ) )
7 exim 1581 . . 3  |-  ( A. x ( ps  ->  ph )  ->  ( E. x ps  ->  E. x ph ) )
86, 7syl 16 . 2  |-  ( A. x ( ph  <->  ps )  ->  ( E. x ps 
->  E. x ph )
)
94, 8impbid 184 1  |-  ( A. x ( ph  <->  ps )  ->  ( E. x ph  <->  E. x ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   A.wal 1546   E.wex 1547
This theorem is referenced by:  exbii  1589  exbidh  1598  exintrbi  1620  19.19  1881  2exbi  27450  rexbidar  27520  onfrALTlem5VD  28710  onfrALTlem1VD  28715  csbxpgVD  28719  csbrngVD  28721  csbunigVD  28723  e2ebindVD  28737  e2ebindALT  28755  bnj956  28857
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563
This theorem depends on definitions:  df-bi 178  df-ex 1548
  Copyright terms: Public domain W3C validator