Metamath Proof Explorer
Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28Jul2009) (Proof shortened by Wolf Lammen, 6Apr2022)


Ref 
Expression 

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

id 
$${\u22a2}{\phi}\to {\phi}$$ 
2 
1

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