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

Theorem exanali 1731
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 431 . . 3  |-  ( (
ph  /\  -.  ps )  <->  -.  ( ph  ->  ps ) )
21exbii 1728 . 2  |-  ( E. x ( ph  /\  -.  ps )  <->  E. x  -.  ( ph  ->  ps ) )
3 exnal 1709 . 2  |-  ( E. x  -.  ( ph  ->  ps )  <->  -.  A. x
( ph  ->  ps )
)
42, 3bitri 257 1  |-  ( E. x ( ph  /\  -.  ps )  <->  -.  A. x
( ph  ->  ps )
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189    /\ wa 375   A.wal 1452   E.wex 1673
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692
This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1674
This theorem is referenced by:  sbn  2230  gencbval  3105  nss  3501  nssss  4669  brprcneu  5880  marypha1lem  7972  reclem2pr  9498  dftr6  30438  brsset  30704  dfon3  30707  dffun10  30729  elfuns  30730  ax12indn  32558  dfss6  36407  vk15.4j  36928  vk15.4jVD  37350
  Copyright terms: Public domain W3C validator