This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ψ → χ

Proof

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