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	⊢ ( ⊥ → 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		fal	⊢ ¬ ⊥
2	1	pm2.21i	⊢ ( ⊥ → 𝜑 )