Metamath Proof Explorer


Theorem mpan2i

Description: An inference based on modus ponens. (Contributed by NM, 10-Apr-1994) (Proof shortened by Wolf Lammen, 19-Nov-2012)

Ref Expression
Hypotheses mpan2i.1 χ
mpan2i.2 φψχθ
Assertion mpan2i φψθ

Proof

Step Hyp Ref Expression
1 mpan2i.1 χ
2 mpan2i.2 φψχθ
3 1 a1i φχ
4 3 2 mpan2d φψθ