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 ψ φ
mpcom.2 φ ψ χ
Assertion mpcom ψ χ


Step Hyp Ref Expression
1 mpcom.1 ψ φ
2 mpcom.2 φ ψ χ
3 2 com12 ψ φ χ
4 1 3 mpd ψ χ