Theorem fal 1574

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

Syntax hints:  ¬ wn 3  ⊤wtru 1561  ⊥wfal 1572

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 1563  df-fal 1573

This theorem is referenced by:  nbfal  1575  bifal  1576  falim  1577  dfnot  1579  notfal  1588  falantru  1595  nffal  1825  alfal  1828  sbn1  2141  nonconne  2969  dfnul3  4289  noel  4290  vn0  4297  falseral0  4468  axnulALT  5254  axnul  5255  canthp1  10612  rlimno1  15681  1stccnp  23522  axnulALT2  35377  axsepg3ALT  35438  nexfal  36765  negsym1  36777  nandsym1  36782  bj-falor  37027  orfa  38581  fald  38628  dihglblem6  41964  ifpdfan  44042  ifpnot  44046  ifpid2  44047  ifpdfxor  44063