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

This theorem is referenced by:  nbfal  1556  bifal  1557  falim  1558  dfnot  1560  notfal  1569  falantru  1576  nffal  1807  alfal  1810  sbn1  2105  nonconne  2952  dfnul3  4326  noel  4330  vn0  4338  csbprc  4406  axnulALT  5304  axnul  5305  canthp1  10648  rlimno1  15599  1stccnp  22965  nexfal  35285  negsym1  35297  nandsym1  35302  bj-falor  35457  orfa  36945  fald  36992  dihglblem6  40206  ifpdfan  42207  ifpnot  42211  ifpid2  42212  ifpdfxor  42228