Theorem ee110 16567

Description: e110 16566 without virtual deductions.

Hypotheses

Ref	Expression
ee110.1	|- (ph -> ps)
ee110.2	|- (ph -> ch)
ee110.3	|- th
ee110.4	|- (ps -> (ch -> (th -> ta)))

Assertion

Ref	Expression
ee110	|- (ph -> ta)

Proof of Theorem ee110

Step	Hyp	Ref	Expression
1		ee110.1	. 2 |- (ph -> ps)
2		ee110.2	. 2 |- (ph -> ch)
3		ee110.3	. . 3 |- th
4	3	a1i 8	. 2 |- (ph -> th)
5		ee110.4	. 2 |- (ps -> (ch -> (th -> ta)))
6	1, 2, 4, 5	syl3c 84	1 |- (ph -> ta)

Syntax hints:   -> wi 3

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7

Copyright terms: Public domain