Metamath Proof Explorer
Description: Simplification of conjunction. (Contributed by Jeff Hankins, 17Nov2009) (Proof shortened by Wolf Lammen, 23Jun2022)


Ref 
Expression 

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

simpr 
$${\u22a2}\left({\phi}\wedge {\chi}\right)\to {\chi}$$ 
2 
1

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