dedlemb

Description: Lemma for weak deduction theorem. See also ifpfal . (Contributed by NM, 15-May-1999) (Proof shortened by Andrew Salmon, 7-May-2011)

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

Step	Hyp	Ref	Expression
1		olc	$⊢ (χ \land \neg φ) \to ((ψ \land φ) \lor (χ \land \neg φ))$
2	1	expcom	$⊢ \neg φ \to (χ \to ((ψ \land φ) \lor (χ \land \neg φ)))$
3		pm2.21	$⊢ \neg φ \to (φ \to χ)$
4	3	adantld	$⊢ \neg φ \to ((ψ \land φ) \to χ)$
5		simpl	$⊢ (χ \land \neg φ) \to χ$
6	5	a1i	$⊢ \neg φ \to ((χ \land \neg φ) \to χ)$
7	4 6	jaod	$⊢ \neg φ \to (((ψ \land φ) \lor (χ \land \neg φ)) \to χ)$
8	2 7	impbid	$⊢ \neg φ \to (χ \leftrightarrow ((ψ \land φ) \lor (χ \land \neg φ)))$

Metamath Proof Explorer