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 φ ψ χ ψ θ χ φ θ

Proof

Step Hyp Ref Expression
1 imim1 φ ψ ψ θ φ θ
2 1 imim2d φ ψ χ ψ θ χ φ θ