3adantll2

Description: Deduction adding a conjunct to antecedent. (Contributed by Glauco Siliprandi, 11-Dec-2019)

		Ref	Expression
	Hypothesis	3adantll2.1	$⊢ (((φ \land ψ) \land χ) \land θ) \to τ$
	Assertion	3adantll2	$⊢ (((φ \land η \land ψ) \land χ) \land θ) \to τ$

Step	Hyp	Ref	Expression
1		3adantll2.1	$⊢ (((φ \land ψ) \land χ) \land θ) \to τ$
2		simpll1	$⊢ (((φ \land η \land ψ) \land χ) \land θ) \to φ$
3		simpll3	$⊢ (((φ \land η \land ψ) \land χ) \land θ) \to ψ$
4	2 3	jca	$⊢ (((φ \land η \land ψ) \land χ) \land θ) \to (φ \land ψ)$
5		simplr	$⊢ (((φ \land η \land ψ) \land χ) \land θ) \to χ$
6		simpr	$⊢ (((φ \land η \land ψ) \land χ) \land θ) \to θ$
7	4 5 6 1	syl21anc	$⊢ (((φ \land η \land ψ) \land χ) \land θ) \to τ$

Metamath Proof Explorer