Theorem fal 1547

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

Syntax hints:  ¬ wn 3  ⊤wtru 1534  ⊥wfal 1545

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 1536  df-fal 1546

This theorem is referenced by:  nbfal  1548  bifal  1549  falim  1550  dfnot  1552  notfal  1561  falantru  1568  nffal  1802  alfal  1805  nonconne  3028  csbprc  4357  axnulALT  5200  axnul  5201  canthp1  10070  rlimno1  15004  1stccnp  22064  nexfal  33748  negsym1  33760  nandsym1  33765  subsym1  33770  bj-falor  33913  orfa  35354  fald  35401  dihglblem6  38470  sbn1  39096  ifpdfan  39824  ifpnot  39828  ifpid2  39829  ifpdfxor  39846