Theorem fal 1554

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

Syntax hints:  ¬ wn 3  ⊤wtru 1541  ⊥wfal 1552

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 207  df-tru 1543  df-fal 1553

This theorem is referenced by:  nbfal  1555  bifal  1556  falim  1557  dfnot  1559  notfal  1568  falantru  1575  nffal  1805  alfal  1808  sbn1  2108  nonconne  2937  dfnul3  4296  noel  4297  vn0  4304  csbprc  4368  axnulALT  5254  axnul  5255  canthp1  10583  rlimno1  15596  1stccnp  23382  axsepg2ALT  35066  nexfal  36386  negsym1  36398  nandsym1  36403  bj-falor  36565  orfa  38069  fald  38116  dihglblem6  41327  ifpdfan  43448  ifpnot  43452  ifpid2  43453  ifpdfxor  43469