Theorem retbwax1 1500

Description: tbw-ax1 1465 rederived from merco1 1478.

This theorem, along with retbwax2 1481, retbwax3 1488, and retbwax4 1480, shows that merco1 1478 with ax-mp 5 can be used as a complete axiomatization of propositional calculus. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
retbwax1	|- ((ph -> ps) -> ((ps -> ch) -> (ph -> ch)))

Proof of Theorem retbwax1

Step	Hyp	Ref	Expression
1		merco1lem18 1499	. . 3 |- ((ps -> (ph -> ch)) -> ((ph -> ps) -> (ph -> ch)))
2		merco1lem16 1497	. . 3 |- (((ps -> (ph -> ch)) -> ((ph -> ps) -> (ph -> ch))) -> ((ps -> ch) -> ((ph -> ps) -> (ph -> ch))))
3	1, 2	ax-mp 5	. 2 |- ((ps -> ch) -> ((ph -> ps) -> (ph -> ch)))
4		merco1lem15 1496	. . . . . 6 |- (((ph -> ps) -> (ph -> ch)) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))
5		merco1lem15 1496	. . . . . 6 |- ((((ph -> ps) -> (ph -> ch)) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch)))) -> (((ph -> ps) -> (ph -> ch)) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))))
6	4, 5	ax-mp 5	. . . . 5 |- (((ph -> ps) -> (ph -> ch)) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch)))))
7		merco1lem18 1499	. . . . 5 |- ((((ph -> ps) -> (ph -> ch)) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> ((((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> (ph -> ch))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))))
8	6, 7	ax-mp 5	. . . 4 |- ((((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> (ph -> ch))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch)))))
9		merco1lem14 1495	. . . 4 |- (((((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> (ph -> ch))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> ((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))))
10	8, 9	ax-mp 5	. . 3 |- ((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch)))))
11		merco1lem14 1495	. . . . . 6 |- (((((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (ph -> ch)) -> ((ps -> ch) -> (ph -> ch)))
12		merco1lem10 1491	. . . . . . . . 9 |- (((((((((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> F. ) -> F. ) -> F. ) -> ((((ps -> ch) -> (ph -> ch)) -> ph) -> F. )) -> ((((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> F. )) -> (((ph -> ch) -> ph) -> ((((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> F. )))
13		merco1 1478	. . . . . . . . 9 |- ((((((((((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> F. ) -> F. ) -> F. ) -> ((((ps -> ch) -> (ph -> ch)) -> ph) -> F. )) -> ((((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> F. )) -> (((ph -> ch) -> ph) -> ((((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> F. ))) -> (((((ph -> ch) -> ph) -> ((((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> F. )) -> (((((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> F. ) -> F. )) -> ((((ps -> ch) -> (ph -> ch)) -> ph) -> (((((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> F. ) -> F. ))))
14	12, 13	ax-mp 5	. . . . . . . 8 |- (((((ph -> ch) -> ph) -> ((((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> F. )) -> (((((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> F. ) -> F. )) -> ((((ps -> ch) -> (ph -> ch)) -> ph) -> (((((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> F. ) -> F. )))
15		merco1 1478	. . . . . . . 8 |- ((((((ph -> ch) -> ph) -> ((((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> F. )) -> (((((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> F. ) -> F. )) -> ((((ps -> ch) -> (ph -> ch)) -> ph) -> (((((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> F. ) -> F. ))) -> ((((((ps -> ch) -> (ph -> ch)) -> ph) -> (((((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> F. ) -> F. )) -> (ph -> ch)) -> ((((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (ph -> ch))))
16	14, 15	ax-mp 5	. . . . . . 7 |- ((((((ps -> ch) -> (ph -> ch)) -> ph) -> (((((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> F. ) -> F. )) -> (ph -> ch)) -> ((((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (ph -> ch)))
17		merco1 1478	. . . . . . 7 |- (((((((ps -> ch) -> (ph -> ch)) -> ph) -> (((((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> F. ) -> F. )) -> (ph -> ch)) -> ((((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (ph -> ch))) -> ((((((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (ph -> ch)) -> ((ps -> ch) -> (ph -> ch))) -> (((((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> F. ) -> ((ps -> ch) -> (ph -> ch)))))
18	16, 17	ax-mp 5	. . . . . 6 |- ((((((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (ph -> ch)) -> ((ps -> ch) -> (ph -> ch))) -> (((((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> F. ) -> ((ps -> ch) -> (ph -> ch))))
19	11, 18	ax-mp 5	. . . . 5 |- (((((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> F. ) -> ((ps -> ch) -> (ph -> ch)))
20		merco1lem15 1496	. . . . 5 |- ((((((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> F. ) -> ((ps -> ch) -> (ph -> ch))) -> (((((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> F. ) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch)))))
21	19, 20	ax-mp 5	. . . 4 |- (((((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> F. ) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))
22		merco1lem10 1491	. . . . . 6 |- ((((((((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> F. ) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch)))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch)))))) -> ((((((((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> F. ) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch)))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch)))))) -> (((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch)))))))
23		merco1lem9 1490	. . . . . 6 |- (((((((((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> F. ) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch)))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch)))))) -> ((((((((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> F. ) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch)))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch)))))) -> (((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))))) -> ((((((((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> F. ) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch)))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch)))))) -> (((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch)))))))
24	22, 23	ax-mp 5	. . . . 5 |- ((((((((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> F. ) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch)))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch)))))) -> (((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))))
25		merco1lem13 1494	. . . . 5 |- (((((((((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> F. ) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch)))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch)))))) -> (((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch)))))) -> ((((((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> F. ) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch)))) -> (((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch)))))))
26	24, 25	ax-mp 5	. . . 4 |- ((((((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> F. ) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch)))) -> (((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))))
27	21, 26	ax-mp 5	. . 3 |- (((ps -> ch) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))) -> (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch)))))
28	10, 27	ax-mp 5	. 2 |- (((ps -> ch) -> ((ph -> ps) -> (ph -> ch))) -> ((ph -> ps) -> ((ps -> ch) -> (ph -> ch))))
29	3, 28	ax-mp 5	1 |- ((ph -> ps) -> ((ps -> ch) -> (ph -> ch)))

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: (None)