Metamath Proof Explorer

Theorem pm3.37

Description: Theorem *3.37 (Transp) of WhiteheadRussell p. 112. (Contributed by NM, 3-Jan-2005) (Proof shortened by Wolf Lammen, 23-Oct-2012)

		Ref	Expression
	Assertion	pm3.37	$⊢ ((φ \land ψ) \to χ) \to ((φ \land \neg χ) \to \neg ψ)$

Step	Hyp	Ref	Expression
1		pm4.14	$⊢ ((φ \land ψ) \to χ) \leftrightarrow ((φ \land \neg χ) \to \neg ψ)$
2	1	biimpi	$⊢ ((φ \land ψ) \to χ) \to ((φ \land \neg χ) \to \neg ψ)$