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 
3adant3r 
$${\u22a2}\left({\phi}\wedge {\psi}\wedge \left({\chi}\wedge {\tau}\right)\right)\to {\theta}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

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

simpl 
$${\u22a2}\left({\chi}\wedge {\tau}\right)\to {\chi}$$ 
3 
2 1

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