Metamath Proof Explorer

Theorem mpani

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

Ref Expression
Hypotheses mpani.1 
|- ps
mpani.2 
|- ( ph -> ( ( ps /\ ch ) -> th ) )
Assertion mpani 
|- ( ph -> ( ch -> th ) )

Proof

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