Metamath Proof Explorer

Theorem mpancom

Description: An inference based on modus ponens with commutation of antecedents. (Contributed by NM, 28-Oct-2003) (Proof shortened by Wolf Lammen, 7-Apr-2013)

Ref Expression
Hypotheses mpancom.1 ψ φ
mpancom.2 φ ψ χ
Assertion mpancom ψ χ


Step Hyp Ref Expression
1 mpancom.1 ψ φ
2 mpancom.2 φ ψ χ
3 id ψ ψ
4 1 3 2 syl2anc ψ χ