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  2944  dfnul3  4289  noel  4290  vn0  4297  csbprc  4361  falseral0  4467  axnulALT  5249  axnul  5250  canthp1  10565  rlimno1  15577  1stccnp  23406  axsepg2ALT  35239  nexfal  36599  negsym1  36611  nandsym1  36616  bj-falor  36784  orfa  38283  fald  38330  dihglblem6  41600  ifpdfan  43707  ifpnot  43711  ifpid2  43712  ifpdfxor  43728