Theorem fal 1530

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

Syntax hints:  ¬ wn 3  ⊤wtru 1524  ⊥wfal 1528

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 1526  df-fal 1529

This theorem is referenced by:  nbfal  1535  bifal  1537  falim  1538  dfnot  1542  falantru  1548  notfal  1559  nffal  1772  nonconne  2835  csbprc  4013  csbprcOLD  4014  axnulALT  4820  axnul  4821  canthp1  9514  rlimno1  14428  1stccnp  21313  alnof  32526  nextf  32530  negsym1  32541  nandsym1  32546  subsym1  32551  bj-falor  32694  orfa  34011  fald  34066  dihglblem6  36946  ifpdfan  38127  ifpnot  38131  ifpid2  38132  ifpdfxor  38149