Theorem fal 1581

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 1571	. . 3 ⊢ ⊤
2	1	notnoti 144	. 2 ⊢ ¬ ¬ ⊤
3		df-fal 1580	. 2 ⊢ (⊥ ↔ ¬ ⊤)
4	2, 3	mtbir 326	1 ⊢ ¬ ⊥

Syntax hints:  ¬ wn 3  ⊤wtru 1568  ⊥wfal 1579

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 210  df-tru 1570  df-fal 1580

This theorem is referenced by:  nbfal  1582  bifal  1583  falim  1584  dfnot  1586  notfal  1595  falantru  1602  nffal  1832  alfal  1835  sbn1  2148  nonconne  2976  dfnul3  4298  noel  4299  vn0  4306  vn0OLD  4307  falseral0  4480  axnulALT  5269  axnul  5270  canthp1  10639  rlimno1  15705  1stccnp  23588  axnulALT2  35415  axsepg3ALT  35478  nexfal  36805  negsym1  36817  nandsym1  36822  bj-falor  37066  bj-vn0ALT  37596  orfa  38621  fald  38668  dihglblem6  42004  ifpdfan  44084  ifpnot  44088  ifpid2  44089  ifpdfxor  44105