New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  alex GIF version

Theorem alex 1572
 Description: Theorem 19.6 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
alex (xφ ↔ ¬ x ¬ φ)

Proof of Theorem alex
StepHypRef Expression
1 notnot 282 . . 3 (φ ↔ ¬ ¬ φ)
21albii 1566 . 2 (xφx ¬ ¬ φ)
3 alnex 1543 . 2 (x ¬ ¬ φ ↔ ¬ x ¬ φ)
42, 3bitri 240 1 (xφ ↔ ¬ x ¬ φ)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 176  ∀wal 1540  ∃wex 1541 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557 This theorem depends on definitions:  df-bi 177  df-ex 1542 This theorem is referenced by:  2nalexn  1573  exnal  1574  19.3v  1665  hba1  1786  exists2  2294  nnsucelrlem1  4424  ltfinex  4464  eqpwrelk  4478  ncfinlowerlem1  4482  eqtfinrelk  4486  evenfinex  4503  oddfinex  4504  evenodddisjlem1  4515  nnadjoinlem1  4519  srelk  4524  sfintfinlem1  4531  tfinnnlem1  4533  dfop2lem1  4573  funsex  5828  qsexg  5982
 Copyright terms: Public domain W3C validator