Metamath Proof Explorer


Theorem pm2.24

Description: Theorem *2.24 of WhiteheadRussell p. 104. Its associated inference is pm2.24i . Commuted form of pm2.21 . (Contributed by NM, 3-Jan-2005)

Ref Expression
Assertion pm2.24
|- ( ph -> ( -. ph -> ps ) )

Proof

Step Hyp Ref Expression
1 pm2.21
 |-  ( -. ph -> ( ph -> ps ) )
2 1 com12
 |-  ( ph -> ( -. ph -> ps ) )