Metamath Proof Explorer

Theorem retbwax3

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

Ref Expression
Assertion retbwax3 
|- ( ( ( ph -> ps ) -> ph ) -> ph )

Proof

Step Hyp Ref Expression
1 retbwax2 
 |-  ( ph -> ( ph -> ph ) )
2 merco1lem7 
 |-  ( ( ph -> ( ph -> ph ) ) -> ( ( ( ph -> ps ) -> ph ) -> ph ) )
3 1 2 ax-mp 
 |-  ( ( ( ph -> ps ) -> ph ) -> ph )