Metamath Proof Explorer
Description: Inference detaching an antecedent and introducing a new one.
(Contributed by Stefan O'Rear, 29Jan2015)


Ref 
Expression 

Hypotheses 
mp1i.1 
$${\u22a2}{\phi}$$ 


mp1i.2 
$${\u22a2}{\phi}\to {\psi}$$ 

Assertion 
mp1i 
$${\u22a2}{\chi}\to {\psi}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

mp1i.1 
$${\u22a2}{\phi}$$ 
2 

mp1i.2 
$${\u22a2}{\phi}\to {\psi}$$ 
3 
1 2

axmp 
$${\u22a2}{\psi}$$ 
4 
3

a1i 
$${\u22a2}{\chi}\to {\psi}$$ 