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

Theorem exbi 1569
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 1547 . . 3  |-  ( A. x ( ph  <->  ps )  ->  A. x ( ph  ->  ps ) )
3 exim 1563 . . 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 1547 . . 3  |-  ( A. x ( ph  <->  ps )  ->  A. x ( ps 
->  ph ) )
7 exim 1563 . . 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 1528   E.wex 1529
This theorem is referenced by:  exbii  1570  exbidh  1579  exintrbi  1601  19.19  1790  2exbi  26977  rexbidar  27048  onfrALTlem5VD  27929  onfrALTlem1VD  27934  csbxpgVD  27938  csbrngVD  27940  csbunigVD  27942  e2ebindVD  27956  e2ebindALT  27974  bnj956  28075
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545
This theorem depends on definitions:  df-bi 179  df-ex 1530
  Copyright terms: Public domain W3C validator