Metamath Proof Explorer
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 |
⊢ ( ( 𝜑 → 𝜓 ) → ( ( 𝜒 → ( 𝜓 → 𝜃 ) ) → ( 𝜒 → ( 𝜑 → 𝜃 ) ) ) ) |