Metamath Proof Explorer

Theorem pm2.521g

Description: A general instance of Theorem *2.521 of WhiteheadRussell p. 107. (Contributed by BJ, 28-Oct-2023)

Ref Expression
Assertion pm2.521g 
|- ( -. ( ph -> ps ) -> ( ps -> ch ) )

Proof

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