Theorem merco1lem1 1479

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

Assertion

Ref	Expression
merco1lem1	|- (ph -> ( F. -> ch))

Proof of Theorem merco1lem1

Step	Hyp	Ref	Expression
1		merco1 1478	. . . . 5 |- ((((( F. -> ph) -> (ph -> F. )) -> (ph -> F. )) -> ( F. -> ph)) -> ((( F. -> ph) -> F. ) -> (ph -> F. )))
2		merco1 1478	. . . . 5 |- (((((( F. -> ph) -> (ph -> F. )) -> (ph -> F. )) -> ( F. -> ph)) -> ((( F. -> ph) -> F. ) -> (ph -> F. ))) -> ((((( F. -> ph) -> F. ) -> (ph -> F. )) -> ( F. -> ph)) -> (ph -> ( F. -> ph))))
3	1, 2	ax-mp 5	. . . 4 |- ((((( F. -> ph) -> F. ) -> (ph -> F. )) -> ( F. -> ph)) -> (ph -> ( F. -> ph)))
4		merco1 1478	. . . 4 |- (((((( F. -> ph) -> F. ) -> (ph -> F. )) -> ( F. -> ph)) -> (ph -> ( F. -> ph))) -> (((ph -> ( F. -> ph)) -> ( F. -> ph)) -> (ph -> ( F. -> ph))))
5	3, 4	ax-mp 5	. . 3 |- (((ph -> ( F. -> ph)) -> ( F. -> ph)) -> (ph -> ( F. -> ph)))
6		merco1 1478	. . . . 5 |- ((((( F. -> ph) -> (ph -> F. )) -> ((ph -> ( F. -> ph)) -> F. )) -> (ph -> ( F. -> ph))) -> (((ph -> ( F. -> ph)) -> F. ) -> (ph -> F. )))
7		merco1 1478	. . . . 5 |- (((((( F. -> ph) -> (ph -> F. )) -> ((ph -> ( F. -> ph)) -> F. )) -> (ph -> ( F. -> ph))) -> (((ph -> ( F. -> ph)) -> F. ) -> (ph -> F. ))) -> (((((ph -> ( F. -> ph)) -> F. ) -> (ph -> F. )) -> ( F. -> ph)) -> ((ph -> ( F. -> ph)) -> ( F. -> ph))))
8	6, 7	ax-mp 5	. . . 4 |- (((((ph -> ( F. -> ph)) -> F. ) -> (ph -> F. )) -> ( F. -> ph)) -> ((ph -> ( F. -> ph)) -> ( F. -> ph)))
9		merco1 1478	. . . 4 |- ((((((ph -> ( F. -> ph)) -> F. ) -> (ph -> F. )) -> ( F. -> ph)) -> ((ph -> ( F. -> ph)) -> ( F. -> ph))) -> ((((ph -> ( F. -> ph)) -> ( F. -> ph)) -> (ph -> ( F. -> ph))) -> (ph -> (ph -> ( F. -> ph)))))
10	8, 9	ax-mp 5	. . 3 |- ((((ph -> ( F. -> ph)) -> ( F. -> ph)) -> (ph -> ( F. -> ph))) -> (ph -> (ph -> ( F. -> ph))))
11	5, 10	ax-mp 5	. 2 |- (ph -> (ph -> ( F. -> ph)))
12		merco1 1478	. . . . 5 |- ((((( F. -> ph) -> (ph -> F. )) -> (ph -> F. )) -> ( F. -> ch)) -> ((( F. -> ch) -> F. ) -> (ph -> F. )))
13		merco1 1478	. . . . 5 |- (((((( F. -> ph) -> (ph -> F. )) -> (ph -> F. )) -> ( F. -> ch)) -> ((( F. -> ch) -> F. ) -> (ph -> F. ))) -> ((((( F. -> ch) -> F. ) -> (ph -> F. )) -> ( F. -> ph)) -> (ph -> ( F. -> ph))))
14	12, 13	ax-mp 5	. . . 4 |- ((((( F. -> ch) -> F. ) -> (ph -> F. )) -> ( F. -> ph)) -> (ph -> ( F. -> ph)))
15		merco1 1478	. . . 4 |- (((((( F. -> ch) -> F. ) -> (ph -> F. )) -> ( F. -> ph)) -> (ph -> ( F. -> ph))) -> (((ph -> ( F. -> ph)) -> ( F. -> ch)) -> (ph -> ( F. -> ch))))
16	14, 15	ax-mp 5	. . 3 |- (((ph -> ( F. -> ph)) -> ( F. -> ch)) -> (ph -> ( F. -> ch)))
17		merco1 1478	. . . . 5 |- ((((( F. -> ch) -> ((ph -> (ph -> ( F. -> ph))) -> F. )) -> ((ph -> ( F. -> ph)) -> F. )) -> (ph -> ( F. -> ch))) -> (((ph -> ( F. -> ch)) -> F. ) -> ((ph -> (ph -> ( F. -> ph))) -> F. )))
18		merco1 1478	. . . . 5 |- (((((( F. -> ch) -> ((ph -> (ph -> ( F. -> ph))) -> F. )) -> ((ph -> ( F. -> ph)) -> F. )) -> (ph -> ( F. -> ch))) -> (((ph -> ( F. -> ch)) -> F. ) -> ((ph -> (ph -> ( F. -> ph))) -> F. ))) -> (((((ph -> ( F. -> ch)) -> F. ) -> ((ph -> (ph -> ( F. -> ph))) -> F. )) -> ( F. -> ch)) -> ((ph -> ( F. -> ph)) -> ( F. -> ch))))
19	17, 18	ax-mp 5	. . . 4 |- (((((ph -> ( F. -> ch)) -> F. ) -> ((ph -> (ph -> ( F. -> ph))) -> F. )) -> ( F. -> ch)) -> ((ph -> ( F. -> ph)) -> ( F. -> ch)))
20		merco1 1478	. . . 4 |- ((((((ph -> ( F. -> ch)) -> F. ) -> ((ph -> (ph -> ( F. -> ph))) -> F. )) -> ( F. -> ch)) -> ((ph -> ( F. -> ph)) -> ( F. -> ch))) -> ((((ph -> ( F. -> ph)) -> ( F. -> ch)) -> (ph -> ( F. -> ch))) -> ((ph -> (ph -> ( F. -> ph))) -> (ph -> ( F. -> ch)))))
21	19, 20	ax-mp 5	. . 3 |- ((((ph -> ( F. -> ph)) -> ( F. -> ch)) -> (ph -> ( F. -> ch))) -> ((ph -> (ph -> ( F. -> ph))) -> (ph -> ( F. -> ch))))
22	16, 21	ax-mp 5	. 2 |- ((ph -> (ph -> ( F. -> ph))) -> (ph -> ( F. -> ch)))
23	11, 22	ax-mp 5	1 |- (ph -> ( F. -> 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:  retbwax4  1480  retbwax2  1481