Theorem exnal 1754

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 1753	. 2 |- ( A. x ph <-> -. E. x -. ph )
2	1	con2bii 347	1 |- ( E. x -. ph <-> -. A. x ph )

Syntax hints:   -. wn 3   <-> wb 196   A.wal 1481   E.wex 1704

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

This theorem depends on definitions:  df-bi 197  df-ex 1705

This theorem is referenced by:  alexn  1771  exanali  1786  19.35  1805  19.30  1809  nfeqf2  2297  nabbi  2896  r2exlem  3059  spc3gv  3298  notzfaus  4840  dtru  4857  eunex  4859  reusv2lem2  4869  reusv2lem2OLD  4870  dtruALT  4899  dvdemo1  4902  dtruALT2  4911  brprcneu  6184  dffv2  6271  zfcndpow  9438  hashfun  13224  nmo  29325  bnj1304  30890  bnj1253  31085  axrepprim  31579  axunprim  31580  axregprim  31582  axinfprim  31583  axacprim  31584  dftr6  31640  brtxpsd  32001  elfuns  32022  dfrdg4  32058  bj-dtru  32797  bj-eunex  32799  bj-dvdemo1  32802  relowlpssretop  33212  wl-dveeq12  33311  clsk3nimkb  38338  vk15.4j  38734  vk15.4jVD  39150  alneu  41201