Theorem 3adantr2

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005)

	Ref	Expression
Hypothesis	3adantr.1	$$⊢\left(\phi \wedge \left(\psi \wedge \chi \right)\right)\to \theta$$
Assertion	3adantr2	$$⊢\left(\phi \wedge \left(\psi \wedge \tau \wedge \chi \right)\right)\to \theta$$

Proof

Step	Hyp	Ref	Expression
1		3adantr.1	$$⊢\left(\phi \wedge \left(\psi \wedge \chi \right)\right)\to \theta$$
2		3simpb	$$⊢\left(\psi \wedge \tau \wedge \chi \right)\to \left(\psi \wedge \chi \right)$$
3	2 1	sylan2	$$⊢\left(\phi \wedge \left(\psi \wedge \tau \wedge \chi \right)\right)\to \theta$$