Theorem fal 1553

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

Syntax hints:  ¬ wn 3  ⊤wtru 1540  ⊥wfal 1551

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 1542  df-fal 1552

This theorem is referenced by:  nbfal  1554  bifal  1555  falim  1556  dfnot  1558  notfal  1567  falantru  1574  nffal  1809  alfal  1812  sbn1  2107  nonconne  2954  dfnul3  4257  noel  4261  vn0  4269  csbprc  4337  axnulALT  5223  axnul  5224  canthp1  10341  rlimno1  15293  1stccnp  22521  nexfal  34521  negsym1  34533  nandsym1  34538  subsym1  34543  bj-falor  34693  orfa  36167  fald  36214  dihglblem6  39281  ifpdfan  40971  ifpnot  40975  ifpid2  40976  ifpdfxor  40992