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 
|- ch
mpan2i.2 
|- ( ph -> ( ( ps /\ ch ) -> th ) )
Assertion mpan2i 
|- ( ph -> ( ps -> th ) )

Proof

Step Hyp Ref Expression
1 mpan2i.1 
 |-  ch
2 mpan2i.2 
 |-  ( ph -> ( ( ps /\ ch ) -> th ) )
3 1 a1i 
 |-  ( ph -> ch )
4 3 2 mpan2d 
 |-  ( ph -> ( ps -> th ) )