NFE Home 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