Theorem re1tbw1

Description: tbw-ax1 rederived from merco2 . (Contributed by Anthony Hart, 16-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	re1tbw1	|- ( ( ph -> ps ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) )

Proof

Step	Hyp	Ref	Expression
1		mercolem8	|- ( ( ph -> ps ) -> ( ( ps -> ( ph -> ch ) ) -> ( ( ph -> ps ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) ) ) )
2		mercolem3	|- ( ( ps -> ch ) -> ( ps -> ( ph -> ch ) ) )
3		mercolem6	|- ( ( ( ph -> ps ) -> ( ( ps -> ( ph -> ch ) ) -> ( ( ph -> ps ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) ) ) ) -> ( ( ps -> ( ph -> ch ) ) -> ( ( ph -> ps ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) ) ) )
4	1 2 3	mpsyl	|- ( ( ps -> ch ) -> ( ( ph -> ps ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) ) )
5		mercolem6	|- ( ( ( ps -> ch ) -> ( ( ph -> ps ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) ) ) -> ( ( ph -> ps ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) ) )
6	4 5	ax-mp	|- ( ( ph -> ps ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) )