Metamath Proof Explorer
Description: An inference based on modus ponens. (Contributed by NM, 16Sep1993)
(Proof shortened by Wolf Lammen, 19Nov2012)


Ref 
Expression 

Hypotheses 
mpan2.1 
$${\u22a2}{\psi}$$ 


mpan2.2 
$${\u22a2}\left({\phi}\wedge {\psi}\right)\to {\chi}$$ 

Assertion 
mpan2 
$${\u22a2}{\phi}\to {\chi}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

mpan2.1 
$${\u22a2}{\psi}$$ 
2 

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

a1i 
$${\u22a2}{\phi}\to {\psi}$$ 
4 
3 2

mpdan 
$${\u22a2}{\phi}\to {\chi}$$ 