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


Ref 
Expression 

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

simpr2 
$${\u22a2}\left({\eta}\wedge \left({\phi}\wedge {\psi}\wedge {\chi}\right)\right)\to {\psi}$$ 
2 
1

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