Theorem fal 1487

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 1484	. . 3 ⊢ ⊤
2	1	notnoti 137	. 2 ⊢ ¬ ¬ ⊤
3		df-fal 1486	. 2 ⊢ (⊥ ↔ ¬ ⊤)
4	2, 3	mtbir 313	1 ⊢ ¬ ⊥

Syntax hints:  ¬ wn 3  ⊤wtru 1481  ⊥wfal 1485

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 197  df-tru 1483  df-fal 1486

This theorem is referenced by:  nbfal  1492  bifal  1494  falim  1495  dfnot  1499  falantru  1505  notfal  1516  nffal  1729  nonconne  2802  csbprc  3958  csbprcOLD  3959  axnulALT  4757  axnul  4758  canthp1  9436  rlimno1  14334  1stccnp  21205  alnof  32096  nextf  32100  negsym1  32111  nandsym1  32116  subsym1  32121  bj-falor  32264  orfa  33552  fald  33607  dihglblem6  36148  ifpdfan  37330  ifpnot  37334  ifpid2  37335  ifpdfxor  37352