Theorem fal 1551

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 1541	. . 3 ⊢ ⊤
2	1	notnoti 145	. 2 ⊢ ¬ ¬ ⊤
3		df-fal 1550	. 2 ⊢ (⊥ ↔ ¬ ⊤)
4	2, 3	mtbir 325	1 ⊢ ¬ ⊥

Syntax hints:  ¬ wn 3  ⊤wtru 1538  ⊥wfal 1549

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 209  df-tru 1540  df-fal 1550

This theorem is referenced by:  nbfal  1552  bifal  1553  falim  1554  dfnot  1556  notfal  1565  falantru  1572  nffal  1806  alfal  1809  nonconne  3028  csbprc  4358  axnulALT  5208  axnul  5209  canthp1  10076  rlimno1  15010  1stccnp  22070  nexfal  33753  negsym1  33765  nandsym1  33770  subsym1  33775  bj-falor  33918  orfa  35375  fald  35422  dihglblem6  38491  sbn1  39122  ifpdfan  39851  ifpnot  39855  ifpid2  39856  ifpdfxor  39873