Theorem fal 1556

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

Syntax hints:  ¬ wn 3  ⊤wtru 1543  ⊥wfal 1554

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 1545  df-fal 1555

This theorem is referenced by:  nbfal  1557  bifal  1558  falim  1559  dfnot  1561  notfal  1570  falantru  1577  nffal  1807  alfal  1810  sbn1  2113  nonconne  2944  dfnul3  4277  noel  4278  vn0  4285  falseral0  4454  axnulALT  5239  axnul  5240  canthp1  10577  rlimno1  15616  1stccnp  23427  axnulALT2  35224  axsepg2ALT  35226  nexfal  36587  negsym1  36599  nandsym1  36604  bj-falor  36849  orfa  38403  fald  38450  dihglblem6  41786  ifpdfan  43893  ifpnot  43897  ifpid2  43898  ifpdfxor  43914