Theorem alnex 1543

Description: Theorem 19.7 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
alnex	⊢ (∀x ¬ φ ↔ ¬ ∃xφ)

Proof of Theorem alnex

Step	Hyp	Ref	Expression
1		df-ex 1542	. 2 ⊢ (∃xφ ↔ ¬ ∀x ¬ φ)
2	1	con2bii 322	1 ⊢ (∀x ¬ φ ↔ ¬ ∃xφ)

Syntax hints:  ¬ wn 3   ↔ wb 176  ∀wal 1540  ∃wex 1541

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

This theorem depends on definitions:  df-bi 177  df-ex 1542

This theorem is referenced by:  nex  1555  alex  1572  exim  1575  alinexa  1578  alexn  1579  nexdh  1589  19.35  1600  19.43  1605  19.43OLD  1606  19.33b  1608  19.38  1794  nf4  1868  mo  2226  mo2  2233  2mo  2282  axi11e  2332  mo2icl  3016  disjsn  3787  dfimak2  4299  iotanul  4355  dm0rn0  4922  dmeq0  4923  imadif  5172