Theorem fal 1539

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 1529	. . 3 ⊢ ⊤
2	1	notnoti 145	. 2 ⊢ ¬ ¬ ⊤
3		df-fal 1538	. 2 ⊢ (⊥ ↔ ¬ ⊤)
4	2, 3	mtbir 324	1 ⊢ ¬ ⊥

Syntax hints:  ¬ wn 3  ⊤wtru 1526  ⊥wfal 1537

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 208  df-tru 1528  df-fal 1538

This theorem is referenced by:  nbfal  1540  bifal  1541  falim  1542  dfnot  1544  notfal  1553  falantru  1560  nffal  1791  alfal  1794  nonconne  2998  csbprc  4284  axnulALT  5106  axnul  5107  canthp1  9929  rlimno1  14848  1stccnp  21758  nexfal  33364  negsym1  33376  nandsym1  33381  subsym1  33386  bj-falor  33529  orfa  34913  fald  34960  dihglblem6  38028  sbn1  38653  ifpdfan  39337  ifpnot  39341  ifpid2  39342  ifpdfxor  39359