Metamath Proof Explorer
Description: Inference chaining two syllogisms syl . Inference associated with
imim12i . (Contributed by NM, 28Dec1992)


Ref 
Expression 

Hypotheses 
3syl.1 
 ( ph > ps ) 


3syl.2 
 ( ps > ch ) 


3syl.3 
 ( ch > th ) 

Assertion 
3syl 
 ( ph > th ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

3syl.1 
 ( ph > ps ) 
2 

3syl.2 
 ( ps > ch ) 
3 

3syl.3 
 ( ch > th ) 
4 
1 2

syl 
 ( ph > ch ) 
5 
4 3

syl 
 ( ph > th ) 