Description: Inference conjoining a theorem to left of consequent in an implication. (Contributed by NM, 31Dec1993)
Ref  Expression  

Hypotheses  jctil.1   ( ph > ps ) 

jctil.2   ch 

Assertion  jctil   ( ph > ( ch /\ ps ) ) 
Step  Hyp  Ref  Expression 

1  jctil.1   ( ph > ps ) 

2  jctil.2   ch 

3  2  a1i   ( ph > ch ) 
4  3 1  jca   ( ph > ( ch /\ ps ) ) 