Theorem fal 1583

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

This proof depends on syntax axioms:  ¬ wn 3  ⊤wtru 1570  ⊥wfal 1581

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-tru 1572  df-fal 1582

This theorem is used by:  nbfal  1584  bifal  1585  falim  1586  dfnot  1588  notfal  1597  falantru  1604  nffal  1837  alfal  1840  sbn1  2145  nonconne  2970  dfnul3  4284  noel  4285  noelOLD  4286  vn0  4293  vn0OLD  4294  falseral0  4472  axnulALT  5260  axnul  5261  canthp1  10749  rlimno1  15833  1stccnp  23793  axnulALT2  35767  axsepg3ALT  35881  nexfal  37320  negsym1  37332  nandsym1  37337  bj-falor  37581  bj-vn0ALT  38126  orfa  39156  fald  39201  dihglblem6  42537  ifpdfan  44607  ifpnot  44611  ifpid2  44612  ifpdfxor  44628