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  2145  nonconne  2973  dfnul3  4293  noel  4294  vn0  4301  vn0OLD  4302  falseral0  4480  axnulALT  5272  axnul  5273  canthp1  10657  rlimno1  15731  1stccnp  23656  axnulALT2  35500  axsepg3ALT  35578  nexfal  36956  negsym1  36968  nandsym1  36973  bj-falor  37217  bj-vn0ALT  37748  orfa  38773  fald  38818  dihglblem6  42154  ifpdfan  44232  ifpnot  44236  ifpid2  44237  ifpdfxor  44253