Theorem efald

Description: Deduction based on reductio ad absurdum. (Contributed by Mario Carneiro, 9-Feb-2017)

	Ref	Expression
Hypothesis	efald.1	⊢ ( ( 𝜑 ∧ ¬ 𝜓 ) → ⊥ )
Assertion	efald	⊢ ( 𝜑 → 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		efald.1	⊢ ( ( 𝜑 ∧ ¬ 𝜓 ) → ⊥ )
2	1	inegd	⊢ ( 𝜑 → ¬ ¬ 𝜓 )
3	2	notnotrd	⊢ ( 𝜑 → 𝜓 )