Metamath Proof Explorer

Theorem re1tbw4

Description: tbw-ax4 rederived from merco2 .

This theorem, along with re1tbw1 , re1tbw2 , and re1tbw3 , shows that merco2 , along with ax-mp , can be used as a complete axiomatization of propositional calculus. (Contributed by Anthony Hart, 16-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion re1tbw4 
|- ( F. -> ph )

Proof

Step Hyp Ref Expression
1 re1tbw3 
 |-  ( ( ( ph -> ph ) -> ph ) -> ph )
2 re1tbw2 
 |-  ( ph -> ( ( ph -> ph ) -> ph ) )
3 re1tbw1 
 |-  ( ( ph -> ( ( ph -> ph ) -> ph ) ) -> ( ( ( ( ph -> ph ) -> ph ) -> ph ) -> ( ph -> ph ) ) )
4 2 3 ax-mp 
 |-  ( ( ( ( ph -> ph ) -> ph ) -> ph ) -> ( ph -> ph ) )
5 1 4 ax-mp 
 |-  ( ph -> ph )
6 re1tbw3 
 |-  ( ( ( ( F. -> ph ) -> ph ) -> ( F. -> ph ) ) -> ( F. -> ph ) )
7 re1tbw2 
 |-  ( ( F. -> ph ) -> ( ( ( F. -> ph ) -> ph ) -> ( F. -> ph ) ) )
8 re1tbw1 
 |-  ( ( ( F. -> ph ) -> ( ( ( F. -> ph ) -> ph ) -> ( F. -> ph ) ) ) -> ( ( ( ( ( F. -> ph ) -> ph ) -> ( F. -> ph ) ) -> ( F. -> ph ) ) -> ( ( F. -> ph ) -> ( F. -> ph ) ) ) )
9 7 8 ax-mp 
 |-  ( ( ( ( ( F. -> ph ) -> ph ) -> ( F. -> ph ) ) -> ( F. -> ph ) ) -> ( ( F. -> ph ) -> ( F. -> ph ) ) )
10 6 9 ax-mp 
 |-  ( ( F. -> ph ) -> ( F. -> ph ) )
11 mercolem3 
 |-  ( ( ( F. -> ph ) -> ph ) -> ( ( F. -> ph ) -> ( F. -> ph ) ) )
12 merco2 
 |-  ( ( ( ( F. -> ph ) -> ph ) -> ( ( F. -> ph ) -> ( F. -> ph ) ) ) -> ( ( ( F. -> ph ) -> ( F. -> ph ) ) -> ( ( ph -> ph ) -> ( ( ph -> ph ) -> ( F. -> ph ) ) ) ) )
13 11 12 ax-mp 
 |-  ( ( ( F. -> ph ) -> ( F. -> ph ) ) -> ( ( ph -> ph ) -> ( ( ph -> ph ) -> ( F. -> ph ) ) ) )
14 10 13 ax-mp 
 |-  ( ( ph -> ph ) -> ( ( ph -> ph ) -> ( F. -> ph ) ) )
15 5 14 ax-mp 
 |-  ( ( ph -> ph ) -> ( F. -> ph ) )
16 5 15 ax-mp 
 |-  ( F. -> ph )