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

Theorem exanali 1572
Description: A transformation of quantifiers and logical connectives. (Contributed by NM, 25-Mar-1996.) (Proof shortened by Wolf Lammen, 4-Sep-2014.)
Assertion
Ref Expression
exanali  |-  ( E. x ( ph  /\  -.  ps )  <->  -.  A. x
( ph  ->  ps )
)

Proof of Theorem exanali
StepHypRef Expression
1 annim 414 . . 3  |-  ( (
ph  /\  -.  ps )  <->  -.  ( ph  ->  ps ) )
21exbii 1569 . 2  |-  ( E. x ( ph  /\  -.  ps )  <->  E. x  -.  ( ph  ->  ps ) )
3 exnal 1561 . 2  |-  ( E. x  -.  ( ph  ->  ps )  <->  -.  A. x
( ph  ->  ps )
)
42, 3bitri 240 1  |-  ( E. x ( ph  /\  -.  ps )  <->  -.  A. x
( ph  ->  ps )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    /\ wa 358   A.wal 1527   E.wex 1528
This theorem is referenced by:  ax11indn  2134  rexnal  2554  gencbval  2832  nss  3236  nssss  4229  brprcneu  5518  marypha1lem  7186  reclem2pr  8672  dftr6  24107  brsset  24429  dfon3  24432  dffun10  24453  elfuns  24454  vk15.4j  28291  vk15.4jVD  28690
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-an 360  df-ex 1529
  Copyright terms: Public domain W3C validator