Theorem merco1lem17 1498

Description: Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1478. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
merco1lem17	|- (((((ph -> ps) -> ph) -> ch) -> ta) -> ((ph -> ch) -> ta))

Proof of Theorem merco1lem17

Step	Hyp	Ref	Expression
1		merco1lem11 1492	. . . . . 6 |- ((((ph -> ps) -> ph) -> ph) -> ((((ch -> ph) -> (((ph -> ps) -> ph) -> F. )) -> F. ) -> ph))
2		merco1lem7 1487	. . . . . . . 8 |- ((((((((ch -> ph) -> (((ph -> ps) -> ph) -> F. )) -> F. ) -> ph) -> ph) -> (((((ph -> ps) -> ph) -> ph) -> ((((ch -> ph) -> (((ph -> ps) -> ph) -> F. )) -> F. ) -> ph)) -> F. )) -> ph) -> (((ph -> ps) -> ph) -> ph))
3		merco1 1478	. . . . . . . 8 |- (((((((((ch -> ph) -> (((ph -> ps) -> ph) -> F. )) -> F. ) -> ph) -> ph) -> (((((ph -> ps) -> ph) -> ph) -> ((((ch -> ph) -> (((ph -> ps) -> ph) -> F. )) -> F. ) -> ph)) -> F. )) -> ph) -> (((ph -> ps) -> ph) -> ph)) -> (((((ph -> ps) -> ph) -> ph) -> ((((ch -> ph) -> (((ph -> ps) -> ph) -> F. )) -> F. ) -> ph)) -> (((((ph -> ps) -> ph) -> ph) -> ((((ch -> ph) -> (((ph -> ps) -> ph) -> F. )) -> F. ) -> ph)) -> ((((ch -> ph) -> (((ph -> ps) -> ph) -> F. )) -> F. ) -> ph))))
4	2, 3	ax-mp 5	. . . . . . 7 |- (((((ph -> ps) -> ph) -> ph) -> ((((ch -> ph) -> (((ph -> ps) -> ph) -> F. )) -> F. ) -> ph)) -> (((((ph -> ps) -> ph) -> ph) -> ((((ch -> ph) -> (((ph -> ps) -> ph) -> F. )) -> F. ) -> ph)) -> ((((ch -> ph) -> (((ph -> ps) -> ph) -> F. )) -> F. ) -> ph)))
5		merco1lem9 1490	. . . . . . 7 |- ((((((ph -> ps) -> ph) -> ph) -> ((((ch -> ph) -> (((ph -> ps) -> ph) -> F. )) -> F. ) -> ph)) -> (((((ph -> ps) -> ph) -> ph) -> ((((ch -> ph) -> (((ph -> ps) -> ph) -> F. )) -> F. ) -> ph)) -> ((((ch -> ph) -> (((ph -> ps) -> ph) -> F. )) -> F. ) -> ph))) -> (((((ph -> ps) -> ph) -> ph) -> ((((ch -> ph) -> (((ph -> ps) -> ph) -> F. )) -> F. ) -> ph)) -> ((((ch -> ph) -> (((ph -> ps) -> ph) -> F. )) -> F. ) -> ph)))
6	4, 5	ax-mp 5	. . . . . 6 |- (((((ph -> ps) -> ph) -> ph) -> ((((ch -> ph) -> (((ph -> ps) -> ph) -> F. )) -> F. ) -> ph)) -> ((((ch -> ph) -> (((ph -> ps) -> ph) -> F. )) -> F. ) -> ph))
7	1, 6	ax-mp 5	. . . . 5 |- ((((ch -> ph) -> (((ph -> ps) -> ph) -> F. )) -> F. ) -> ph)
8		merco1 1478	. . . . 5 |- (((((ch -> ph) -> (((ph -> ps) -> ph) -> F. )) -> F. ) -> ph) -> ((ph -> ch) -> (((ph -> ps) -> ph) -> ch)))
9	7, 8	ax-mp 5	. . . 4 |- ((ph -> ch) -> (((ph -> ps) -> ph) -> ch))
10		merco1lem11 1492	. . . . . 6 |- (((((ph -> ch) -> F. ) -> (ph -> ch)) -> (ph -> ch)) -> (((((((ph -> ps) -> ph) -> ch) -> ph) -> ((((ph -> ch) -> F. ) -> (ph -> ch)) -> F. )) -> F. ) -> (ph -> ch)))
11		merco1lem7 1487	. . . . . . . 8 |- (((((((((((ph -> ps) -> ph) -> ch) -> ph) -> ((((ph -> ch) -> F. ) -> (ph -> ch)) -> F. )) -> F. ) -> (ph -> ch)) -> ph) -> ((((((ph -> ch) -> F. ) -> (ph -> ch)) -> (ph -> ch)) -> (((((((ph -> ps) -> ph) -> ch) -> ph) -> ((((ph -> ch) -> F. ) -> (ph -> ch)) -> F. )) -> F. ) -> (ph -> ch))) -> F. )) -> ph) -> ((((ph -> ch) -> F. ) -> (ph -> ch)) -> (ph -> ch)))
12		merco1 1478	. . . . . . . 8 |- ((((((((((((ph -> ps) -> ph) -> ch) -> ph) -> ((((ph -> ch) -> F. ) -> (ph -> ch)) -> F. )) -> F. ) -> (ph -> ch)) -> ph) -> ((((((ph -> ch) -> F. ) -> (ph -> ch)) -> (ph -> ch)) -> (((((((ph -> ps) -> ph) -> ch) -> ph) -> ((((ph -> ch) -> F. ) -> (ph -> ch)) -> F. )) -> F. ) -> (ph -> ch))) -> F. )) -> ph) -> ((((ph -> ch) -> F. ) -> (ph -> ch)) -> (ph -> ch))) -> ((((((ph -> ch) -> F. ) -> (ph -> ch)) -> (ph -> ch)) -> (((((((ph -> ps) -> ph) -> ch) -> ph) -> ((((ph -> ch) -> F. ) -> (ph -> ch)) -> F. )) -> F. ) -> (ph -> ch))) -> ((((((ph -> ch) -> F. ) -> (ph -> ch)) -> (ph -> ch)) -> (((((((ph -> ps) -> ph) -> ch) -> ph) -> ((((ph -> ch) -> F. ) -> (ph -> ch)) -> F. )) -> F. ) -> (ph -> ch))) -> (((((((ph -> ps) -> ph) -> ch) -> ph) -> ((((ph -> ch) -> F. ) -> (ph -> ch)) -> F. )) -> F. ) -> (ph -> ch)))))
13	11, 12	ax-mp 5	. . . . . . 7 |- ((((((ph -> ch) -> F. ) -> (ph -> ch)) -> (ph -> ch)) -> (((((((ph -> ps) -> ph) -> ch) -> ph) -> ((((ph -> ch) -> F. ) -> (ph -> ch)) -> F. )) -> F. ) -> (ph -> ch))) -> ((((((ph -> ch) -> F. ) -> (ph -> ch)) -> (ph -> ch)) -> (((((((ph -> ps) -> ph) -> ch) -> ph) -> ((((ph -> ch) -> F. ) -> (ph -> ch)) -> F. )) -> F. ) -> (ph -> ch))) -> (((((((ph -> ps) -> ph) -> ch) -> ph) -> ((((ph -> ch) -> F. ) -> (ph -> ch)) -> F. )) -> F. ) -> (ph -> ch))))
14		merco1lem9 1490	. . . . . . 7 |- (((((((ph -> ch) -> F. ) -> (ph -> ch)) -> (ph -> ch)) -> (((((((ph -> ps) -> ph) -> ch) -> ph) -> ((((ph -> ch) -> F. ) -> (ph -> ch)) -> F. )) -> F. ) -> (ph -> ch))) -> ((((((ph -> ch) -> F. ) -> (ph -> ch)) -> (ph -> ch)) -> (((((((ph -> ps) -> ph) -> ch) -> ph) -> ((((ph -> ch) -> F. ) -> (ph -> ch)) -> F. )) -> F. ) -> (ph -> ch))) -> (((((((ph -> ps) -> ph) -> ch) -> ph) -> ((((ph -> ch) -> F. ) -> (ph -> ch)) -> F. )) -> F. ) -> (ph -> ch)))) -> ((((((ph -> ch) -> F. ) -> (ph -> ch)) -> (ph -> ch)) -> (((((((ph -> ps) -> ph) -> ch) -> ph) -> ((((ph -> ch) -> F. ) -> (ph -> ch)) -> F. )) -> F. ) -> (ph -> ch))) -> (((((((ph -> ps) -> ph) -> ch) -> ph) -> ((((ph -> ch) -> F. ) -> (ph -> ch)) -> F. )) -> F. ) -> (ph -> ch))))
15	13, 14	ax-mp 5	. . . . . 6 |- ((((((ph -> ch) -> F. ) -> (ph -> ch)) -> (ph -> ch)) -> (((((((ph -> ps) -> ph) -> ch) -> ph) -> ((((ph -> ch) -> F. ) -> (ph -> ch)) -> F. )) -> F. ) -> (ph -> ch))) -> (((((((ph -> ps) -> ph) -> ch) -> ph) -> ((((ph -> ch) -> F. ) -> (ph -> ch)) -> F. )) -> F. ) -> (ph -> ch)))
16	10, 15	ax-mp 5	. . . . 5 |- (((((((ph -> ps) -> ph) -> ch) -> ph) -> ((((ph -> ch) -> F. ) -> (ph -> ch)) -> F. )) -> F. ) -> (ph -> ch))
17		merco1 1478	. . . . 5 |- ((((((((ph -> ps) -> ph) -> ch) -> ph) -> ((((ph -> ch) -> F. ) -> (ph -> ch)) -> F. )) -> F. ) -> (ph -> ch)) -> (((ph -> ch) -> (((ph -> ps) -> ph) -> ch)) -> ((((ph -> ch) -> F. ) -> (ph -> ch)) -> (((ph -> ps) -> ph) -> ch))))
18	16, 17	ax-mp 5	. . . 4 |- (((ph -> ch) -> (((ph -> ps) -> ph) -> ch)) -> ((((ph -> ch) -> F. ) -> (ph -> ch)) -> (((ph -> ps) -> ph) -> ch)))
19	9, 18	ax-mp 5	. . 3 |- ((((ph -> ch) -> F. ) -> (ph -> ch)) -> (((ph -> ps) -> ph) -> ch))
20		merco1lem4 1484	. . 3 |- ((((ta -> ph) -> ((ph -> ch) -> F. )) -> ch) -> (((ph -> ch) -> F. ) -> ch))
21		merco1lem16 1497	. . 3 |- (((((ph -> ch) -> F. ) -> (ph -> ch)) -> (((ph -> ps) -> ph) -> ch)) -> ((((ph -> ch) -> F. ) -> ch) -> (((ph -> ps) -> ph) -> ch)))
22	19, 20, 21	mpsyl 59	. 2 |- ((((ta -> ph) -> ((ph -> ch) -> F. )) -> ch) -> (((ph -> ps) -> ph) -> ch))
23		merco1 1478	. 2 |- (((((ta -> ph) -> ((ph -> ch) -> F. )) -> ch) -> (((ph -> ps) -> ph) -> ch)) -> (((((ph -> ps) -> ph) -> ch) -> ta) -> ((ph -> ch) -> ta)))
24	22, 23	ax-mp 5	1 |- (((((ph -> ps) -> ph) -> ch) -> ta) -> ((ph -> ch) -> ta))

Syntax hints:   -> wi 4   F. wfal 1317

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-tru 1319  df-fal 1320

This theorem is referenced by:  merco1lem18  1499