Theorem fal 1555

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

Syntax hints:  ¬ wn 3  ⊤wtru 1542  ⊥wfal 1553

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 1544  df-fal 1554

This theorem is referenced by:  nbfal  1556  bifal  1557  falim  1558  dfnot  1560  notfal  1569  falantru  1576  nffal  1806  alfal  1809  sbn1  2110  nonconne  2940  dfnul3  4284  noel  4285  vn0  4292  csbprc  4356  axnulALT  5240  axnul  5241  canthp1  10545  rlimno1  15561  1stccnp  23377  axsepg2ALT  35095  nexfal  36449  negsym1  36461  nandsym1  36466  bj-falor  36628  orfa  38132  fald  38179  dihglblem6  41449  ifpdfan  43569  ifpnot  43573  ifpid2  43574  ifpdfxor  43590