Theorem falim

Description: The truth value F. implies anything. Also called the "principle of explosion", or "ex falso [sequitur] quodlibet" (Latin for "from falsehood, anything [follows]"). Dual statement of trud . (Contributed by FL, 20-Mar-2011) (Proof shortened by Anthony Hart, 1-Aug-2011)

	Ref	Expression
Assertion	falim	$$⊢\perp \to \phi$$

Proof

Step	Hyp	Ref	Expression
1		fal	$$⊢\neg \perp$$
2	1	pm2.21i	$$⊢\perp \to \phi$$