Mathbox for BJ 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > Mathboxes > bjcon2com  Structured version Unicode version 
Description: A commuted form of the contrapositive, true in minimal calculus. (Contributed by BJ, 19Mar2020.) 
Ref  Expression 

bjcon2com 
Step  Hyp  Ref  Expression 

1  con2 119  . 2  
2  1  com12 32  1 
Colors of variables: wff setvar class 
Syntax hints: wn 3 wi 4 
This theorem was proved from axioms: axmp 5 ax1 6 ax2 7 ax3 8 
This theorem is referenced by: bjcon2comi 30920 
Copyright terms: Public domain  W3C validator 