Theorem fal 1584

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

This proof depends on syntax axioms:  ¬ wn 3  ⊤wtru 1571  ⊥wfal 1582

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-tru 1573  df-fal 1583

This theorem is used by:  nbfal  1585  bifal  1586  falim  1587  dfnot  1589  notfal  1598  falantru  1605  nffal  1838  alfal  1841  sbn1  2144  nonconne  2968  dfnul3  4283  noel  4284  vn0  4291  vn0OLD  4292  falseral0  4470  axnulALT  5258  axnul  5259  canthp1  10739  rlimno1  15821  1stccnp  23781  axnulALT2  35712  axsepg3ALT  35810  nexfal  37193  negsym1  37205  nandsym1  37210  bj-falor  37454  bj-vn0ALT  37987  orfa  39016  fald  39061  dihglblem6  42397  ifpdfan  44466  ifpnot  44470  ifpid2  44471  ifpdfxor  44487