Metamath Proof Explorer

Theorem eel2122old

Description: el2122old without virtual deductions. (Contributed by Alan Sare, 13-Jun-2015) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	eel2122old.1	$⊢ (φ \land ψ) \to χ$
		eel2122old.2	$⊢ ψ \to θ$
		eel2122old.3	$⊢ ψ \to τ$
		eel2122old.4	$⊢ (χ \land θ \land τ) \to η$
	Assertion	eel2122old	$⊢ (φ \land ψ) \to η$

Proof

Step	Hyp	Ref	Expression
1		eel2122old.1	$⊢ (φ \land ψ) \to χ$
2		eel2122old.2	$⊢ ψ \to θ$
3		eel2122old.3	$⊢ ψ \to τ$
4		eel2122old.4	$⊢ (χ \land θ \land τ) \to η$
5	4	3exp	$⊢ χ \to (θ \to (τ \to η))$
6	1 5	syl	$⊢ (φ \land ψ) \to (θ \to (τ \to η))$
7	2 6	syl5	$⊢ (φ \land ψ) \to (ψ \to (τ \to η))$
8	3 7	syl7	$⊢ (φ \land ψ) \to (ψ \to (ψ \to η))$
9	8	ex	$⊢ φ \to (ψ \to (ψ \to (ψ \to η)))$
10	9	pm2.43d	$⊢ φ \to (ψ \to (ψ \to η))$
11	10	pm2.43d	$⊢ φ \to (ψ \to η)$
12	11	imp	$⊢ (φ \land ψ) \to η$