Metamath Proof Explorer
Description: A double modus ponens inference. (Contributed by Mario Carneiro, 24Jan2013)


Ref 
Expression 

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


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


mp2b.3 
$${\u22a2}{\psi}\to {\chi}$$ 

Assertion 
mp2b 
$${\u22a2}{\chi}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

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

mp2b.2 
$${\u22a2}{\phi}\to {\psi}$$ 
3 

mp2b.3 
$${\u22a2}{\psi}\to {\chi}$$ 
4 
1 2

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

axmp 
$${\u22a2}{\chi}$$ 