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  2941  dfnul3  4286  noel  4287  vn0  4294  csbprc  4358  axnulALT  5244  axnul  5245  canthp1  10552  rlimno1  15563  1stccnp  23378  axsepg2ALT  35116  nexfal  36470  negsym1  36482  nandsym1  36487  bj-falor  36649  orfa  38142  fald  38189  dihglblem6  41459  ifpdfan  43583  ifpnot  43587  ifpid2  43588  ifpdfxor  43604