Metamath Proof Explorer
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 19Oct1999) (Proof shortened by Wolf Lammen, 20Nov2012)


Ref 
Expression 

Hypothesis 
ad2ant.1 
$${\u22a2}{\phi}\to {\psi}$$ 

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

ad2ant.1 
$${\u22a2}{\phi}\to {\psi}$$ 
2 
1

adantr 
$${\u22a2}\left({\phi}\wedge {\theta}\right)\to {\psi}$$ 
3 
2

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