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

Step	Hyp	Ref	Expression
1		annim 425	. . 3
2	1	exbii 1667	. 2
3		exnal 1648	. 2
4	2, 3	bitri 249	1

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