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

Metamath Proof Explorer

Theorem mpan

Description: An inference based on modus ponens. (Contributed by NM, 30-Aug-1993) (Proof shortened by Wolf Lammen, 7-Apr-2013)

Ref Expression
Hypotheses mpan.1 ⊢ φ
mpan.2 ⊢ φ ∧ ψ → χ
Assertion mpan ⊢ ψ → χ

Proof

Step Hyp Ref Expression
1 mpan.1 ⊢ φ
2 mpan.2 ⊢ φ ∧ ψ → χ
3 1 a1i ⊢ ψ → φ
4 3 2 mpancom ⊢ ψ → χ