Description: Inference that swaps (commutes) antecedents in an implication. Inference associated with pm2.04 . Its associated inference is mpi . (Contributed by NM, 29Dec1992) (Proof shortened by Wolf Lammen, 4Aug2012)
Ref  Expression  

Hypothesis  com12.1   ( ph > ( ps > ch ) ) 

Assertion  com12   ( ps > ( ph > ch ) ) 
Step  Hyp  Ref  Expression 

1  com12.1   ( ph > ( ps > ch ) ) 

2  id   ( ps > ps ) 

3  2 1  syl5com   ( ps > ( ph > ch ) ) 