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	|- ( ( ph /\ ps ) -> ch )
	eel2122old.2	|- ( ps -> th )
	eel2122old.3	|- ( ps -> ta )
	eel2122old.4	|- ( ( ch /\ th /\ ta ) -> et )
Assertion	eel2122old	|- ( ( ph /\ ps ) -> et )

Proof

Step	Hyp	Ref	Expression
1		eel2122old.1	|- ( ( ph /\ ps ) -> ch )
2		eel2122old.2	|- ( ps -> th )
3		eel2122old.3	|- ( ps -> ta )
4		eel2122old.4	|- ( ( ch /\ th /\ ta ) -> et )
5	4	3exp	|- ( ch -> ( th -> ( ta -> et ) ) )
6	1 5	syl	|- ( ( ph /\ ps ) -> ( th -> ( ta -> et ) ) )
7	2 6	syl5	|- ( ( ph /\ ps ) -> ( ps -> ( ta -> et ) ) )
8	3 7	syl7	|- ( ( ph /\ ps ) -> ( ps -> ( ps -> et ) ) )
9	8	ex	|- ( ph -> ( ps -> ( ps -> ( ps -> et ) ) ) )
10	9	pm2.43d	|- ( ph -> ( ps -> ( ps -> et ) ) )
11	10	pm2.43d	|- ( ph -> ( ps -> et ) )
12	11	imp	|- ( ( ph /\ ps ) -> et )