Theorem efald2

Description: A proof by contradiction. (Contributed by Giovanni Mascellani, 15-Sep-2017)

	Ref	Expression
Hypothesis	efald2.1	$$⊢\neg \phi \to \perp$$
Assertion	efald2	$$⊢\phi$$

Proof

Step	Hyp	Ref	Expression
1		efald2.1	$$⊢\neg \phi \to \perp$$
2	1	adantl	$$⊢\left(\top \wedge \neg \phi \right)\to \perp$$
3	2	efald	$$⊢\top \to \phi$$
4	3	mptru	$$⊢\phi$$