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

Theorem exanali 1595
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 415 . . 3  |-  ( (
ph  /\  -.  ps )  <->  -.  ( ph  ->  ps ) )
21exbii 1592 . 2  |-  ( E. x ( ph  /\  -.  ps )  <->  E. x  -.  ( ph  ->  ps ) )
3 exnal 1583 . 2  |-  ( E. x  -.  ( ph  ->  ps )  <->  -.  A. x
( ph  ->  ps )
)
42, 3bitri 241 1  |-  ( E. x ( ph  /\  -.  ps )  <->  -.  A. x
( ph  ->  ps )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    /\ wa 359   A.wal 1549   E.wex 1550
This theorem is referenced by:  sbn  2130  ax11indn  2272  rexnal  2716  gencbval  3000  nss  3406  nssss  4419  brprcneu  5721  marypha1lem  7438  reclem2pr  8925  dftr6  25373  brsset  25734  dfon3  25737  dffun10  25759  elfuns  25760  vk15.4j  28612  vk15.4jVD  29026
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551
  Copyright terms: Public domain W3C validator