Theorem merco1lem18 1499

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
merco1lem18	|- ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))

Proof of Theorem merco1lem18

Step	Hyp	Ref	Expression
1		merco1 1478	. . . 4 |- ((((((ps -> ch) -> ps) -> ((ps -> ph) -> F. )) -> ((ps -> ch) -> ps)) -> ph) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch))))
2		merco1lem17 1498	. . . 4 |- (((((((ps -> ch) -> ps) -> ((ps -> ph) -> F. )) -> ((ps -> ch) -> ps)) -> ph) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))) -> ((((ps -> ch) -> ps) -> ph) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))))
3	1, 2	ax-mp 5	. . 3 |- ((((ps -> ch) -> ps) -> ph) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch))))
4		merco1lem17 1498	. . 3 |- (((((ps -> ch) -> ps) -> ph) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))) -> ((ps -> ph) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))))
5	3, 4	ax-mp 5	. 2 |- ((ps -> ph) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch))))
6		merco1lem5 1485	. . . . . . 7 |- ((((((((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch))) -> F. ) -> (((ps -> ph) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))) -> F. )) -> F. ) -> F. ) -> F. ) -> (((((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch))) -> F. ) -> (((ps -> ph) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))) -> F. )) -> F. ))
7		merco1lem3 1483	. . . . . . 7 |- (((((((((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch))) -> F. ) -> (((ps -> ph) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))) -> F. )) -> F. ) -> F. ) -> F. ) -> (((((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch))) -> F. ) -> (((ps -> ph) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))) -> F. )) -> F. )) -> (((((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch))) -> F. ) -> (((ps -> ph) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))) -> F. )) -> ((((((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch))) -> F. ) -> (((ps -> ph) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))) -> F. )) -> F. ) -> F. )))
8	6, 7	ax-mp 5	. . . . . 6 |- (((((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch))) -> F. ) -> (((ps -> ph) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))) -> F. )) -> ((((((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch))) -> F. ) -> (((ps -> ph) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))) -> F. )) -> F. ) -> F. ))
9		merco1lem5 1485	. . . . . 6 |- ((((((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch))) -> F. ) -> (((ps -> ph) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))) -> F. )) -> ((((((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch))) -> F. ) -> (((ps -> ph) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))) -> F. )) -> F. ) -> F. )) -> (((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch))) -> ((((((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch))) -> F. ) -> (((ps -> ph) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))) -> F. )) -> F. ) -> F. )))
10	8, 9	ax-mp 5	. . . . 5 |- (((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch))) -> ((((((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch))) -> F. ) -> (((ps -> ph) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))) -> F. )) -> F. ) -> F. ))
11		merco1lem4 1484	. . . . 5 |- ((((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch))) -> ((((((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch))) -> F. ) -> (((ps -> ph) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))) -> F. )) -> F. ) -> F. )) -> (((ps -> ph) -> (ps -> ch)) -> ((((((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch))) -> F. ) -> (((ps -> ph) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))) -> F. )) -> F. ) -> F. )))
12	10, 11	ax-mp 5	. . . 4 |- (((ps -> ph) -> (ps -> ch)) -> ((((((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch))) -> F. ) -> (((ps -> ph) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))) -> F. )) -> F. ) -> F. ))
13		merco1 1478	. . . . 5 |- (((((((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch))) -> F. ) -> (((ps -> ph) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))) -> F. )) -> F. ) -> (ps -> ph)) -> (((ps -> ph) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))) -> (((ps -> ph) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch))))))
14		merco1lem2 1482	. . . . 5 |- ((((((((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch))) -> F. ) -> (((ps -> ph) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))) -> F. )) -> F. ) -> (ps -> ph)) -> (((ps -> ph) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))) -> (((ps -> ph) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))))) -> ((((ps -> ph) -> (ps -> ch)) -> ((((((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch))) -> F. ) -> (((ps -> ph) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))) -> F. )) -> F. ) -> F. )) -> (((ps -> ph) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))) -> (((ps -> ph) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))))))
15	13, 14	ax-mp 5	. . . 4 |- ((((ps -> ph) -> (ps -> ch)) -> ((((((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch))) -> F. ) -> (((ps -> ph) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))) -> F. )) -> F. ) -> F. )) -> (((ps -> ph) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))) -> (((ps -> ph) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch))))))
16	12, 15	ax-mp 5	. . 3 |- (((ps -> ph) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))) -> (((ps -> ph) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))))
17		merco1lem9 1490	. . 3 |- ((((ps -> ph) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))) -> (((ps -> ph) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch))))) -> (((ps -> ph) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))))
18	16, 17	ax-mp 5	. 2 |- (((ps -> ph) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch)))) -> ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> ch))))
19	5, 18	ax-mp 5	1 |- ((ph -> (ps -> ch)) -> ((ps -> ph) -> (ps -> 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:  retbwax1  1500