Metamath Proof Explorer

Theorem bj-imim11

Description: The propositional function ( ( . -> ph ) -> ps ) is increasing. (Contributed by BJ, 3-Apr-2026)

Ref Expression
Assertion bj-imim11 
|- ( ( ph -> ps ) -> ( ( ( ph -> ch ) -> th ) -> ( ( ps -> ch ) -> th ) ) )

Proof

Step Hyp Ref Expression
1 imim1 
 |-  ( ( ph -> ps ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) )
2 1 imim1d 
 |-  ( ( ph -> ps ) -> ( ( ( ph -> ch ) -> th ) -> ( ( ps -> ch ) -> th ) ) )