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

This theorem is referenced by:  nbfal  1555  bifal  1556  falim  1557  dfnot  1559  notfal  1568  falantru  1575  nffal  1806  alfal  1809  sbn1  2104  nonconne  2952  dfnul3  4270  noel  4274  vn0  4282  csbprc  4350  axnulALT  5242  axnul  5243  canthp1  10489  rlimno1  15441  1stccnp  22693  nexfal  34664  negsym1  34676  nandsym1  34681  bj-falor  34836  orfa  36317  fald  36364  dihglblem6  39580  ifpdfan  41312  ifpnot  41316  ifpid2  41317  ifpdfxor  41333