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  4710  axnul  4711  canthp1  9333  rlimno1  14181  1stccnp  21023  rusgra0edg  26276  alnof  31365  nextf  31369  negsym1  31380  nandsym1  31385  subsym1  31390  bj-falor  31536  bj-nffal  31569  orfa  32845  fald  32900  dihglblem6  35441  ifpdfan  36623  ifpnot  36627  ifpid2  36628  ifpdfxor  36645