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 323	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  1808  alfal  1811  sbn1  2106  nonconne  2956  dfnul3  4261  noel  4265  vn0  4273  csbprc  4341  axnulALT  5229  axnul  5230  canthp1  10419  rlimno1  15374  1stccnp  22622  nexfal  34603  negsym1  34615  nandsym1  34620  subsym1  34625  bj-falor  34775  orfa  36249  fald  36296  dihglblem6  39361  ifpdfan  41080  ifpnot  41084  ifpid2  41085  ifpdfxor  41101