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

Metamath Proof Explorer

Theorem mpan2

Description: An inference based on modus ponens. (Contributed by NM, 16-Sep-1993) (Proof shortened by Wolf Lammen, 19-Nov-2012)

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

Proof

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