Theorem fal 1556

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

Syntax hints:  ¬ wn 3  ⊤wtru 1543  ⊥wfal 1554

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 1545  df-fal 1555

This theorem is referenced by:  nbfal  1557  bifal  1558  falim  1559  dfnot  1561  notfal  1570  falantru  1577  nffal  1807  alfal  1810  sbn1  2113  nonconne  2945  dfnul3  4278  noel  4279  vn0  4286  falseral0  4455  axnulALT  5240  axnul  5241  canthp1  10571  rlimno1  15610  1stccnp  23440  axnulALT2  35243  axsepg2ALT  35245  nexfal  36606  negsym1  36618  nandsym1  36623  bj-falor  36868  orfa  38420  fald  38467  dihglblem6  41803  ifpdfan  43914  ifpnot  43918  ifpid2  43919  ifpdfxor  43935