Metamath Proof Explorer

Theorem pm4.14

Description: Theorem *4.14 of WhiteheadRussell p. 117. Related to con34b . (Contributed by NM, 3-Jan-2005) (Proof shortened by Wolf Lammen, 23-Oct-2012)

		Ref	Expression
	Assertion	pm4.14	$⊢ ((φ \land ψ) \to χ) \leftrightarrow ((φ \land \neg χ) \to \neg ψ)$

Proof

Step	Hyp	Ref	Expression
1		con34b	$⊢ (ψ \to χ) \leftrightarrow (\neg χ \to \neg ψ)$
2	1	imbi2i	$⊢ (φ \to (ψ \to χ)) \leftrightarrow (φ \to (\neg χ \to \neg ψ))$
3		impexp	$⊢ ((φ \land ψ) \to χ) \leftrightarrow (φ \to (ψ \to χ))$
4		impexp	$⊢ ((φ \land \neg χ) \to \neg ψ) \leftrightarrow (φ \to (\neg χ \to \neg ψ))$
5	2 3 4	3bitr4i	$⊢ ((φ \land ψ) \to χ) \leftrightarrow ((φ \land \neg χ) \to \neg ψ)$