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  2249  rexnal  2681  gencbval  2964  nss  3370  nssss  4383  brprcneu  5684  marypha1lem  7400  reclem2pr  8885  dftr6  25325  brsset  25647  dfon3  25650  dffun10  25671  elfuns  25672  vk15.4j  28327  vk15.4jVD  28739
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