Metamath Proof Explorer

Theorem adh-minimp-pm2.43

Description: Derivation of pm2.43 WhiteheadRussell p. 106 (also called "hilbert" or "W") from adh-minimp-ax1 , adh-minimp-ax2 , and ax-mp . It uses the derivation written DD22D21 in D-notation. (See head comment for an explanation.) Polish prefix notation: CCpCpqCpq . (Contributed by BJ, 31-May-2021) (Revised by ADH, 10-Nov-2023) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion adh-minimp-pm2.43 
|- ( ( ph -> ( ph -> ps ) ) -> ( ph -> ps ) )

Proof

Step Hyp Ref Expression
1 adh-minimp-ax1 
 |-  ( ph -> ( ( ph -> ps ) -> ph ) )
2 adh-minimp-ax2 
 |-  ( ( ph -> ( ( ph -> ps ) -> ph ) ) -> ( ( ph -> ( ph -> ps ) ) -> ( ph -> ph ) ) )
3 1 2 ax-mp 
 |-  ( ( ph -> ( ph -> ps ) ) -> ( ph -> ph ) )
4 adh-minimp-ax2 
 |-  ( ( ph -> ( ph -> ps ) ) -> ( ( ph -> ph ) -> ( ph -> ps ) ) )
5 adh-minimp-ax2 
 |-  ( ( ( ph -> ( ph -> ps ) ) -> ( ( ph -> ph ) -> ( ph -> ps ) ) ) -> ( ( ( ph -> ( ph -> ps ) ) -> ( ph -> ph ) ) -> ( ( ph -> ( ph -> ps ) ) -> ( ph -> ps ) ) ) )
6 4 5 ax-mp 
 |-  ( ( ( ph -> ( ph -> ps ) ) -> ( ph -> ph ) ) -> ( ( ph -> ( ph -> ps ) ) -> ( ph -> ps ) ) )
7 3 6 ax-mp 
 |-  ( ( ph -> ( ph -> ps ) ) -> ( ph -> ps ) )