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  1874  2exbi  27249  rexbidar  27319  onfrALTlem5VD  28340  onfrALTlem1VD  28345  csbxpgVD  28349  csbrngVD  28351  csbunigVD  28353  e2ebindVD  28367  e2ebindALT  28385  bnj956  28487
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