Metamath Proof Explorer
Description: Importation inference. (Contributed by NM, 8Apr1994) (Proof
shortened by Wolf Lammen, 20Jun2022)


Ref 
Expression 

Hypothesis 
3imp.1 
$${\u22a2}{\phi}\to \left({\psi}\to \left({\chi}\to {\theta}\right)\right)$$ 

Assertion 
3imp 
$${\u22a2}\left({\phi}\wedge {\psi}\wedge {\chi}\right)\to {\theta}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

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

imp31 
$${\u22a2}\left(\left({\phi}\wedge {\psi}\right)\wedge {\chi}\right)\to {\theta}$$ 
3 
2

3impa 
$${\u22a2}\left({\phi}\wedge {\psi}\wedge {\chi}\right)\to {\theta}$$ 