Theorem fal 1584

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

This proof depends on syntax axioms:  ¬ wn 3  ⊤wtru 1571  ⊥wfal 1582

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

This theorem is used by:  nbfal  1585  bifal  1586  falim  1587  dfnot  1589  notfal  1598  falantru  1605  nffal  1838  alfal  1841  sbn1  2145  nonconne  2972  dfnul3  4290  noel  4291  vn0  4298  vn0OLD  4299  falseral0  4477  axnulALT  5269  axnul  5270  canthp1  10656  rlimno1  15731  1stccnp  23672  axnulALT2  35536  axsepg3ALT  35614  nexfal  36975  negsym1  36987  nandsym1  36992  bj-falor  37236  bj-vn0ALT  37767  orfa  38793  fald  38838  dihglblem6  42174  ifpdfan  44252  ifpnot  44256  ifpid2  44257  ifpdfxor  44273