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

This theorem is referenced by:  nbfal  1554  bifal  1555  falim  1556  dfnot  1558  notfal  1567  falantru  1574  nffal  1804  alfal  1807  sbn1  2106  nonconne  2951  dfnul3  4336  noel  4337  vn0  4344  csbprc  4408  axnulALT  5303  axnul  5304  canthp1  10695  rlimno1  15691  1stccnp  23471  axsepg2ALT  35098  nexfal  36407  negsym1  36419  nandsym1  36424  bj-falor  36586  orfa  38090  fald  38137  dihglblem6  41343  ifpdfan  43484  ifpnot  43488  ifpid2  43489  ifpdfxor  43505