Theorem fal 1482

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 1479	. . 3 ⊢ ⊤
2	1	notnoti 136	. 2 ⊢ ¬ ¬ ⊤
3		df-fal 1481	. 2 ⊢ (⊥ ↔ ¬ ⊤)
4	2, 3	mtbir 312	1 ⊢ ¬ ⊥

Syntax hints:  ¬ wn 3  ⊤wtru 1476  ⊥wfal 1480

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 196  df-tru 1478  df-fal 1481

This theorem is referenced by:  nbfal  1486  bifal  1488  falim  1489  dfnot  1493  falantru  1499  notfal  1510  nffal  1723  nonconne  2794  csbprc  3932  csbprcOLD  3933  axnulALT  4715  axnul  4716  canthp1  9355  rlimno1  14232  1stccnp  21075  rusgra0edg  26482  alnof  31571  nextf  31575  negsym1  31586  nandsym1  31591  subsym1  31596  bj-falor  31742  bj-nffal  31775  orfa  33051  fald  33106  dihglblem6  35647  ifpdfan  36829  ifpnot  36833  ifpid2  36834  ifpdfxor  36851