Metamath Proof Explorer
Description: Modus tollens inference. (Contributed by NM, 26Mar1995) (Proof
shortened by Wolf Lammen, 15Sep2012)


Ref 
Expression 

Hypotheses 
mt3i.1 
$${\u22a2}\neg {\chi}$$ 


mt3i.2 
$${\u22a2}{\phi}\to \left(\neg {\psi}\to {\chi}\right)$$ 

Assertion 
mt3i 
$${\u22a2}{\phi}\to {\psi}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

mt3i.1 
$${\u22a2}\neg {\chi}$$ 
2 

mt3i.2 
$${\u22a2}{\phi}\to \left(\neg {\psi}\to {\chi}\right)$$ 
3 
1

a1i 
$${\u22a2}{\phi}\to \neg {\chi}$$ 
4 
3 2

mt3d 
$${\u22a2}{\phi}\to {\psi}$$ 