Mathbox for Alan Sare 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > Mathboxes > con5  Unicode version 
Description: Biconditional contraposition variation. This proof is con5VD 28992 automatically translated and minimized. (Contributed by Alan Sare, 21Apr2013.) (Proof modification is discouraged.) (New usage is discouraged.) 
Ref  Expression 

con5 
Step  Hyp  Ref  Expression 

1  bi2 189  . 2  
2  1  con1d 116  1 
Colors of variables: wff set class 
Syntax hints: wn 3 wi 4 wb 176 
This theorem is referenced by: con5i 28585 
This theorem was proved from axioms: ax1 5 ax2 6 ax3 7 axmp 8 
This theorem depends on definitions: dfbi 177 
Copyright terms: Public domain  W3C validator 