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  2112  nonconne  2942  dfnul3  4287  noel  4288  vn0  4295  csbprc  4359  falseral0  4465  axnulALT  5247  axnul  5248  canthp1  10563  rlimno1  15575  1stccnp  23404  axsepg2ALT  35188  nexfal  36548  negsym1  36560  nandsym1  36565  bj-falor  36727  orfa  38222  fald  38269  dihglblem6  41539  ifpdfan  43649  ifpnot  43653  ifpid2  43654  ifpdfxor  43670