This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pm5.44

Description: Theorem *5.44 of WhiteheadRussell p. 125. (Contributed by NM, 3-Jan-2005)

		Ref	Expression
	Assertion	pm5.44	$⊢ (φ \to ψ) \to ((φ \to χ) \leftrightarrow (φ \to (ψ \land χ)))$

Step	Hyp	Ref	Expression
1		jcab	$⊢ (φ \to (ψ \land χ)) \leftrightarrow ((φ \to ψ) \land (φ \to χ))$
2	1	baibr	$⊢ (φ \to ψ) \to ((φ \to χ) \leftrightarrow (φ \to (ψ \land χ)))$