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	|- ( F. -> ph )

Proof

Step	Hyp	Ref	Expression
1		fal	|- -. F.
2	1	pm2.21i	|- ( F. -> ph )