dedlem0b

Description: Lemma for an alternate version of weak deduction theorem. (Contributed by NM, 2-Apr-1994)

		Ref	Expression
	Assertion	dedlem0b	$⊢ \neg φ \to (ψ \leftrightarrow ((ψ \to φ) \to (χ \land φ)))$

Step	Hyp	Ref	Expression
1		pm2.21	$⊢ \neg φ \to (φ \to (χ \land φ))$
2	1	imim2d	$⊢ \neg φ \to ((ψ \to φ) \to (ψ \to (χ \land φ)))$
3	2	com23	$⊢ \neg φ \to (ψ \to ((ψ \to φ) \to (χ \land φ)))$
4		pm2.21	$⊢ \neg ψ \to (ψ \to φ)$
5		simpr	$⊢ (χ \land φ) \to φ$
6	4 5	imim12i	$⊢ ((ψ \to φ) \to (χ \land φ)) \to (\neg ψ \to φ)$
7	6	con1d	$⊢ ((ψ \to φ) \to (χ \land φ)) \to (\neg φ \to ψ)$
8	7	com12	$⊢ \neg φ \to (((ψ \to φ) \to (χ \land φ)) \to ψ)$
9	3 8	impbid	$⊢ \neg φ \to (ψ \leftrightarrow ((ψ \to φ) \to (χ \land φ)))$

Metamath Proof Explorer