Theorem 3adantr3

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	3adantr3	$$⊢\left(\phi \wedge \left(\psi \wedge \chi \wedge \tau \right)\right)\to \theta$$

Proof

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