Theorem fal 1561

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 1551	. . 3 ⊢ ⊤
2	1	notnoti 143	. 2 ⊢ ¬ ¬ ⊤
3		df-fal 1560	. 2 ⊢ (⊥ ↔ ¬ ⊤)
4	2, 3	mtbir 324	1 ⊢ ¬ ⊥

Syntax hints:  ¬ wn 3  ⊤wtru 1548  ⊥wfal 1559

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 208  df-tru 1550  df-fal 1560

This theorem is referenced by:  nbfal  1562  bifal  1563  falim  1564  dfnot  1566  notfal  1575  falantru  1582  nffal  1812  alfal  1815  sbn1  2118  nonconne  2946  dfnul3  4265  noel  4266  vn0  4273  falseral0  4442  axnulALT  5226  axnul  5227  canthp1  10568  rlimno1  15607  1stccnp  23445  axnulALT2  35264  axsepg3ALT  35323  nexfal  36633  negsym1  36645  nandsym1  36650  bj-falor  36895  orfa  38449  fald  38496  dihglblem6  41832  ifpdfan  43910  ifpnot  43914  ifpid2  43915  ifpdfxor  43931