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  2945  dfnul3  4291  noel  4292  vn0  4299  csbprc  4363  falseral0  4469  axnulALT  5251  axnul  5252  canthp1  10577  rlimno1  15589  1stccnp  23418  axnulALT2  35258  axsepg2ALT  35260  nexfal  36621  negsym1  36633  nandsym1  36638  bj-falor  36809  orfa  38333  fald  38380  dihglblem6  41716  ifpdfan  43822  ifpnot  43826  ifpid2  43827  ifpdfxor  43843