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 28346 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 190  . 2  
2  1  con1d 118  1 
Colors of variables: wff set class 
Syntax hints: wn 3 wi 4 wb 177 
This theorem is referenced by: con5i 27943 
This theorem was proved from axioms: ax1 5 ax2 6 ax3 7 axmp 8 
This theorem depends on definitions: dfbi 178 
Copyright terms: Public domain  W3C validator 