Metamath Proof Explorer
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8Jan2006) (Proof shortened by Wolf Lammen, 25Jun2022)


Ref 
Expression 

Hypothesis 
ad4ant3.1 
$${\u22a2}\left({\phi}\wedge {\psi}\wedge {\chi}\right)\to {\theta}$$ 

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

ad4ant3.1 
$${\u22a2}\left({\phi}\wedge {\psi}\wedge {\chi}\right)\to {\theta}$$ 
2 

simpr 
$${\u22a2}\left({\tau}\wedge {\psi}\right)\to {\psi}$$ 
3 
2 1

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