Mathbox for Alan Sare 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > Mathboxes > con5i  Unicode version 
Description: Inference form of con5 28584. (Contributed by Alan Sare, 21Apr2013.) (Proof modification is discouraged.) (New usage is discouraged.) 
Ref  Expression 

con5i.1 
Ref  Expression 

con5i 
Step  Hyp  Ref  Expression 

1  con5i.1  . 2  
2  con5 28584  . 2  
3  1, 2  axmp 8  1 
Colors of variables: wff set class 
Syntax hints: wn 3 wi 4 wb 176 
This theorem is referenced by: vk15.4j 28590 vk15.4jVD 29006 
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 