Theorem exnal 1707

Description: Theorem 19.14 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)

Assertion

Ref	Expression
exnal	|- ( E. x -. ph <-> -. A. x ph )

Proof of Theorem exnal

Step	Hyp	Ref	Expression
1		alex 1706	. 2 |- ( A. x ph <-> -. E. x -. ph )
2	1	con2bii 339	1 |- ( E. x -. ph <-> -. A. x ph )

Syntax hints:   -. wn 3   <-> wb 189   A.wal 1450   E.wex 1671

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690

This theorem depends on definitions:  df-bi 190  df-ex 1672

This theorem is referenced by:  alexn  1722  exanali  1729  19.35  1748  19.30  1752  excomOLD  1945  nfeqf2  2148  nabbi  2744  r2exlem  2899  spc3gv  3125  notzfaus  4576  dtru  4592  eunex  4594  reusv2lem2  4603  dtruALT  4632  dvdemo1  4635  dtruALT2  4644  brprcneu  5872  dffv2  5953  zfcndpow  9059  hashfun  12650  nmo  28200  bnj1304  29703  bnj1253  29898  axrepprim  30401  axunprim  30402  axregprim  30404  axinfprim  30405  axacprim  30406  dftr6  30461  brtxpsd  30732  elfuns  30753  dfrdg4  30789  bj-dtru  31478  bj-eunex  31480  bj-dvdemo1  31483  relowlpssretop  31837  vk15.4j  36955  vk15.4jVD  37374  alneu  38767