Theorem fal 1631

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

Syntax hints:  ¬ wn 3  ⊤wtru 1625  ⊥wfal 1629

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 1627  df-fal 1630

This theorem is referenced by:  nbfal  1636  bifal  1638  falim  1639  dfnot  1643  falantru  1649  notfal  1660  nffal  1873  nonconne  2936  csbprc  4115  csbprcOLD  4116  axnulALT  4931  axnul  4932  canthp1  9660  rlimno1  14575  1stccnp  21459  alnof  32699  nextf  32703  negsym1  32714  nandsym1  32719  subsym1  32724  bj-falor  32867  orfa  34186  fald  34241  dihglblem6  37123  ifpdfan  38304  ifpnot  38308  ifpid2  38309  ifpdfxor  38326