dedlema

Description: Lemma for weak deduction theorem. See also ifptru . (Contributed by NM, 26-Jun-2002) (Proof shortened by Andrew Salmon, 7-May-2011)

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

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

Metamath Proof Explorer