Theorem fal 1551

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 1541	. . 3 ⊢ ⊤
2	1	notnoti 143	. 2 ⊢ ¬ ¬ ⊤
3		df-fal 1550	. 2 ⊢ (⊥ ↔ ¬ ⊤)
4	2, 3	mtbir 323	1 ⊢ ¬ ⊥

Syntax hints:  ¬ wn 3  ⊤wtru 1538  ⊥wfal 1549

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 207  df-tru 1540  df-fal 1550

This theorem is referenced by:  nbfal  1552  bifal  1553  falim  1554  dfnot  1556  notfal  1565  falantru  1572  nffal  1802  alfal  1805  sbn1  2105  nonconne  2950  dfnul3  4343  noel  4344  vn0  4351  csbprc  4415  axnulALT  5310  axnul  5311  canthp1  10692  rlimno1  15687  1stccnp  23486  axsepg2ALT  35076  nexfal  36388  negsym1  36400  nandsym1  36405  bj-falor  36567  orfa  38069  fald  38116  dihglblem6  41323  ifpdfan  43456  ifpnot  43460  ifpid2  43461  ifpdfxor  43477