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  2146  nonconne  2971  dfnul3  4285  noel  4286  noelOLD  4287  vn0  4294  vn0OLD  4295  falseral0  4473  axnulALT  5264  axnul  5265  canthp1  10778  rlimno1  15865  1stccnp  23836  axnulALT2  35825  axsepg3ALT  35951  nexfal  37408  negsym1  37420  nandsym1  37425  bj-falor  37669  bj-vn0ALT  38257  orfa  39282  fald  39327  dihglblem6  42663  ifpdfan  44728  ifpnot  44732  ifpid2  44733  ifpdfxor  44749