Metamath Proof Explorer
Description: Deduction adding three conjuncts to antecedent. (Contributed by Mario
Carneiro, 5Jan2017) (Proof shortened by Wolf Lammen, 5Apr2022)


Ref 
Expression 

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

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

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

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

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