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	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜒 )
	eel2122old.2	⊢ ( 𝜓 → 𝜃 )
	eel2122old.3	⊢ ( 𝜓 → 𝜏 )
	eel2122old.4	⊢ ( ( 𝜒 ∧ 𝜃 ∧ 𝜏 ) → 𝜂 )
Assertion	eel2122old	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜂 )

Proof

Step	Hyp	Ref	Expression
1		eel2122old.1	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜒 )
2		eel2122old.2	⊢ ( 𝜓 → 𝜃 )
3		eel2122old.3	⊢ ( 𝜓 → 𝜏 )
4		eel2122old.4	⊢ ( ( 𝜒 ∧ 𝜃 ∧ 𝜏 ) → 𝜂 )
5	4	3exp	⊢ ( 𝜒 → ( 𝜃 → ( 𝜏 → 𝜂 ) ) )
6	1 5	syl	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝜃 → ( 𝜏 → 𝜂 ) ) )
7	2 6	syl5	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝜓 → ( 𝜏 → 𝜂 ) ) )
8	3 7	syl7	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝜓 → ( 𝜓 → 𝜂 ) ) )
9	8	ex	⊢ ( 𝜑 → ( 𝜓 → ( 𝜓 → ( 𝜓 → 𝜂 ) ) ) )
10	9	pm2.43d	⊢ ( 𝜑 → ( 𝜓 → ( 𝜓 → 𝜂 ) ) )
11	10	pm2.43d	⊢ ( 𝜑 → ( 𝜓 → 𝜂 ) )
12	11	imp	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜂 )