Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > syl6ci  Structured version Unicode version 
Description: A syllogism inference combined with contraction. (Contributed by Alan Sare, 18Mar2012.) 
Ref  Expression 

syl6ci.1  
syl6ci.2  
syl6ci.3 
Ref  Expression 

syl6ci 
Step  Hyp  Ref  Expression 

1  syl6ci.1  . 2  
2  syl6ci.2  . . 3  
3  2  a1d 25  . 2 
4  syl6ci.3  . 2  
5  1, 3, 4  syl6c 64  1 
Colors of variables: wff setvar class 
Syntax hints: wi 4 
This theorem was proved from axioms: axmp 5 ax1 6 ax2 7 
This theorem is referenced by: omeulem2 7027 btwnconn1lem12 28134 sbcim2g 31250 ee21an 31470 
Copyright terms: Public domain  W3C validator 