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


Ref 
Expression 

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

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

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