Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > mt4  Unicode version 
Description: The rule of modus tollens. (Contributed by Wolf Lammen, 12May2013.) 
Ref  Expression 

mt4.1  
mt4.2 
Ref  Expression 

mt4 
Step  Hyp  Ref  Expression 

1  mt4.1  . 2  
2  mt4.2  . . 3  
3  2  con4i 122  . 2 
4  1, 3  axmp 8  1 
Colors of variables: wff set class 
Syntax hints: wn 3 wi 4 
This theorem is referenced by: infeq5i 7353 chirredi 22990 
This theorem was proved from axioms: ax1 5 ax2 6 ax3 7 axmp 8 
Copyright terms: Public domain  W3C validator 