Metamath Proof Explorer
Description: Simplification of conjunction. (Contributed by NM, 9Mar2012) (Proof
shortened by Wolf Lammen, 23Jun2022)


Ref 
Expression 

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

simpll 
$${\u22a2}\left(\left({\phi}\wedge {\psi}\right)\wedge {\tau}\right)\to {\phi}$$ 
2 
1

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