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  2967  dfnul3  4283  noel  4284  vn0  4291  vn0OLD  4292  falseral0  4470  axnulALT  5261  axnul  5262  canthp1  10664  rlimno1  15742  1stccnp  23689  axnulALT2  35591  axsepg3ALT  35669  nexfal  37025  negsym1  37037  nandsym1  37042  bj-falor  37286  bj-vn0ALT  37817  orfa  38833  fald  38878  dihglblem6  42214  ifpdfan  44307  ifpnot  44311  ifpid2  44312  ifpdfxor  44328