Theorem fal 1556

Description: The truth value ⊥ is refutable. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Mel L. O'Cat, 11-Mar-2012.)

Assertion

Ref	Expression
fal	⊢ ¬ ⊥

Proof of Theorem fal

Step	Hyp	Ref	Expression
1		tru 1546	. . 3 ⊢ ⊤
2	1	notnoti 143	. 2 ⊢ ¬ ¬ ⊤
3		df-fal 1555	. 2 ⊢ (⊥ ↔ ¬ ⊤)
4	2, 3	mtbir 323	1 ⊢ ¬ ⊥

Syntax hints:  ¬ wn 3  ⊤wtru 1543  ⊥wfal 1554

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 206  df-tru 1545  df-fal 1555

This theorem is referenced by:  nbfal  1557  bifal  1558  falim  1559  dfnot  1561  notfal  1570  falantru  1577  nffal  1808  alfal  1811  sbn1  2106  nonconne  2953  dfnul3  4327  noel  4331  vn0  4339  csbprc  4407  axnulALT  5305  axnul  5306  canthp1  10649  rlimno1  15600  1stccnp  22966  nexfal  35290  negsym1  35302  nandsym1  35307  bj-falor  35462  orfa  36950  fald  36997  dihglblem6  40211  ifpdfan  42217  ifpnot  42221  ifpid2  42222  ifpdfxor  42238