Description: Inference introducing an antecedent. Inference associated with ax1 . Its associated inference is a1ii . See conventions for a definition of "associated inference". (Contributed by NM, 29Dec1992)
Ref  Expression  

Hypothesis  a1i.1   ph 

Assertion  a1i   ( ps > ph ) 
Step  Hyp  Ref  Expression 

1  a1i.1   ph 

2  ax1   ( ph > ( ps > ph ) ) 

3  1 2  axmp   ( ps > ph ) 