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

Theorem exanali 1592
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 1589 . 2  |-  ( E. x ( ph  /\  -.  ps )  <->  E. x  -.  ( ph  ->  ps ) )
3 exnal 1580 . 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 1546   E.wex 1547
This theorem is referenced by:  ax11indn  2245  rexnal  2677  gencbval  2960  nss  3366  nssss  4379  brprcneu  5680  marypha1lem  7396  reclem2pr  8881  dftr6  25321  brsset  25643  dfon3  25646  dffun10  25667  elfuns  25668  vk15.4j  28323  vk15.4jVD  28735
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-an 361  df-ex 1548
  Copyright terms: Public domain W3C validator