Metamath Proof Explorer

Theorem bj-imim21

Description: The propositional function ( ch -> ( . -> th ) ) is decreasing. (Contributed by BJ, 19-Jul-2019)

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

Proof

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