Metamath Proof Explorer

Theorem mt4i

Description: Modus tollens inference. (Contributed by Wolf Lammen, 12-May-2013)

Ref Expression
Hypotheses mt4i.1 
|- ch
mt4i.2 
|- ( ph -> ( -. ps -> -. ch ) )
Assertion mt4i 
|- ( ph -> ps )

Proof

Step Hyp Ref Expression
1 mt4i.1 
 |-  ch
2 mt4i.2 
 |-  ( ph -> ( -. ps -> -. ch ) )
3 1 a1i 
 |-  ( ph -> ch )
4 3 2 mt4d 
 |-  ( ph -> ps )