Metamath Proof Explorer
Description: Simplification of triple conjunction. (Contributed by NM, 21Apr1994)
(Proof shortened by Wolf Lammen, 22Jun2022)


Ref 
Expression 

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

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

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