Metamath Proof Explorer

Theorem adh-minim-pm2.43

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

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

Proof

Step Hyp Ref Expression
1 adh-minim-ax1 
 |-  ( ph -> ( ( ph -> ps ) -> ph ) )
2 adh-minim-ax2 
 |-  ( ( ph -> ( ( ph -> ps ) -> ph ) ) -> ( ( ph -> ( ph -> ps ) ) -> ( ph -> ph ) ) )
3 1 2 ax-mp 
 |-  ( ( ph -> ( ph -> ps ) ) -> ( ph -> ph ) )
4 adh-minim-ax2 
 |-  ( ( ph -> ( ph -> ps ) ) -> ( ( ph -> ph ) -> ( ph -> ps ) ) )
5 adh-minim-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 ) )