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 
|- ( ph -> ( ( ps -> -. ph ) -> -. ps ) )

Proof

Step Hyp Ref Expression
1 con2 
 |-  ( ( ps -> -. ph ) -> ( ph -> -. ps ) )
2 1 com12 
 |-  ( ph -> ( ( ps -> -. ph ) -> -. ps ) )