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 ⊢ ¬ ⊥

Syntax hints:  ¬ wn 3  ⊤wtru 1571  ⊥wfal 1582

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 1573  df-fal 1583

This theorem is referenced by:  nbfal  1585  bifal  1586  falim  1587  dfnot  1589  notfal  1598  falantru  1605  nffal  1835  alfal  1838  sbn1  2142  nonconne  2970  dfnul3  4290  noel  4291  vn0  4298  vn0OLD  4299  falseral0  4475  axnulALT  5267  axnul  5268  canthp1  10634  rlimno1  15701  1stccnp  23619  axnulALT2  35471  axsepg3ALT  35555  nexfal  36936  negsym1  36948  nandsym1  36953  bj-falor  37197  bj-vn0ALT  37728  orfa  38753  fald  38798  dihglblem6  42134  ifpdfan  44212  ifpnot  44216  ifpid2  44217  ifpdfxor  44233