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

Theorem exanali 1670
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

Proof of Theorem exanali
StepHypRef Expression
1 annim 425 . . 3
21exbii 1667 . 2
3 exnal 1648 . 2
42, 3bitri 249 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184  /\wa 369  A.wal 1393  E.wex 1612
This theorem is referenced by:  sbn  2132  ax12indn  2273  rexnalOLD  2906  gencbval  3155  nss  3561  nssss  4708  brprcneu  5864  marypha1lem  7913  reclem2pr  9447  dftr6  29179  brsset  29539  dfon3  29542  dffun10  29564  elfuns  29565  vk15.4j  33298  vk15.4jVD  33714  dfss6  37792
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613
  Copyright terms: Public domain W3C validator