Theorem fal 1551

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 1541	. . 3 ⊢ ⊤
2	1	notnoti 143	. 2 ⊢ ¬ ¬ ⊤
3		df-fal 1550	. 2 ⊢ (⊥ ↔ ¬ ⊤)
4	2, 3	mtbir 323	1 ⊢ ¬ ⊥

Syntax hints:  ¬ wn 3  ⊤wtru 1538  ⊥wfal 1549

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 1540  df-fal 1550

This theorem is referenced by:  nbfal  1552  bifal  1553  falim  1554  dfnot  1556  notfal  1565  falantru  1572  nffal  1803  alfal  1806  sbn1  2107  nonconne  2958  dfnul3  4356  noel  4360  vn0  4368  csbprc  4432  axnulALT  5322  axnul  5323  canthp1  10723  rlimno1  15702  1stccnp  23491  axsepg2ALT  35059  nexfal  36371  negsym1  36383  nandsym1  36388  bj-falor  36550  orfa  38042  fald  38089  dihglblem6  41297  ifpdfan  43428  ifpnot  43432  ifpid2  43433  ifpdfxor  43449