Metamath Proof Explorer

Theorem bj-con2com

Description: A commuted form of the contrapositive, true in minimal calculus. (Contributed by BJ, 19-Mar-2020)

Ref Expression
Assertion bj-con2com ( 𝜑 → ( ( 𝜓 → ¬ 𝜑 ) → ¬ 𝜓 ) )

Proof

Step Hyp Ref Expression
1 con2 ⊢ ( ( 𝜓 → ¬ 𝜑 ) → ( 𝜑 → ¬ 𝜓 ) )
2 1 com12 ⊢ ( 𝜑 → ( ( 𝜓 → ¬ 𝜑 ) → ¬ 𝜓 ) )