Metamath Proof Explorer

Theorem mpcom

Description: Modus ponens inference with commutation of antecedents. Commuted form of mpd . (Contributed by NM, 17-Mar-1996)

Ref Expression
Hypotheses mpcom.1 
|- ( ps -> ph )
mpcom.2 
|- ( ph -> ( ps -> ch ) )
Assertion mpcom 
|- ( ps -> ch )

Proof

Step Hyp Ref Expression
1 mpcom.1 
 |-  ( ps -> ph )
2 mpcom.2 
 |-  ( ph -> ( ps -> ch ) )
3 2 com12 
 |-  ( ps -> ( ph -> ch ) )
4 1 3 mpd 
 |-  ( ps -> ch )