Theorem retbwax2 1481

Description: tbw-ax2 1466 rederived from merco1 1478. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
retbwax2	|- (ph -> (ps -> ph))

Proof of Theorem retbwax2

Step	Hyp	Ref	Expression
1		merco1lem1 1479	. . . 4 |- (((((ph -> ph) -> ph) -> (ph -> F. )) -> ph) -> ( F. -> ph))
2		merco1 1478	. . . 4 |- ((((((ph -> ph) -> ph) -> (ph -> F. )) -> ph) -> ( F. -> ph)) -> ((( F. -> ph) -> (ph -> ph)) -> (ph -> (ph -> ph))))
3	1, 2	ax-mp 5	. . 3 |- ((( F. -> ph) -> (ph -> ph)) -> (ph -> (ph -> ph)))
4		merco1 1478	. . . 4 |- (((((ph -> (ph -> ph)) -> (ph -> F. )) -> (ph -> F. )) -> F. ) -> (( F. -> ph) -> (ph -> ph)))
5		merco1 1478	. . . 4 |- ((((((ph -> (ph -> ph)) -> (ph -> F. )) -> (ph -> F. )) -> F. ) -> (( F. -> ph) -> (ph -> ph))) -> (((( F. -> ph) -> (ph -> ph)) -> (ph -> (ph -> ph))) -> (ph -> (ph -> (ph -> ph)))))
6	4, 5	ax-mp 5	. . 3 |- (((( F. -> ph) -> (ph -> ph)) -> (ph -> (ph -> ph))) -> (ph -> (ph -> (ph -> ph))))
7	3, 6	ax-mp 5	. 2 |- (ph -> (ph -> (ph -> ph)))
8		merco1lem1 1479	. . . 4 |- (((((ps -> ph) -> ph) -> (ph -> F. )) -> ph) -> ( F. -> ph))
9		merco1 1478	. . . 4 |- ((((((ps -> ph) -> ph) -> (ph -> F. )) -> ph) -> ( F. -> ph)) -> ((( F. -> ph) -> (ps -> ph)) -> (ph -> (ps -> ph))))
10	8, 9	ax-mp 5	. . 3 |- ((( F. -> ph) -> (ps -> ph)) -> (ph -> (ps -> ph)))
11		merco1 1478	. . . 4 |- (((((ph -> (ps -> ph)) -> (ps -> F. )) -> ((ph -> (ph -> (ph -> ph))) -> F. )) -> F. ) -> (( F. -> ph) -> (ps -> ph)))
12		merco1 1478	. . . 4 |- ((((((ph -> (ps -> ph)) -> (ps -> F. )) -> ((ph -> (ph -> (ph -> ph))) -> F. )) -> F. ) -> (( F. -> ph) -> (ps -> ph))) -> (((( F. -> ph) -> (ps -> ph)) -> (ph -> (ps -> ph))) -> ((ph -> (ph -> (ph -> ph))) -> (ph -> (ps -> ph)))))
13	11, 12	ax-mp 5	. . 3 |- (((( F. -> ph) -> (ps -> ph)) -> (ph -> (ps -> ph))) -> ((ph -> (ph -> (ph -> ph))) -> (ph -> (ps -> ph))))
14	10, 13	ax-mp 5	. 2 |- ((ph -> (ph -> (ph -> ph))) -> (ph -> (ps -> ph)))
15	7, 14	ax-mp 5	1 |- (ph -> (ps -> ph))

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:  merco1lem2  1482  merco1lem3  1483  retbwax3  1488