Theorem exnal 1618

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

Syntax hints:   -. wn 3   <-> wb 184   A.wal 1367   E.wex 1586

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

This theorem depends on definitions:  df-bi 185  df-ex 1587

This theorem is referenced by:  alexn  1631  exanali  1637  19.35  1654  19.30  1659  excom  1787  nfeqf2  1989  nabbi  2701  spc3gv  3057  notzfaus  4462  dtru  4478  eunex  4480  reusv2lem2  4489  dtruALT  4519  dvdemo1  4522  dtruALT2  4531  brprcneu  5679  dffv2  5759  zfcndpow  8775  hashfun  12191  nmo  25837  axrepprim  27322  axunprim  27323  axregprim  27325  axinfprim  27326  axacprim  27327  dftr6  27529  brtxpsd  27894  elfuns  27915  dfrdg4  27950  alneu  29996  vk15.4j  31162  vk15.4jVD  31579  bnj1304  31742  bnj1253  31937  bj-dtru  32219  bj-eunex  32221  bj-dvdemo1  32224