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 φ ψ θ