3adantlr3

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

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

Step	Hyp	Ref	Expression
1		3adantlr3.1	$⊢ ((φ \land (ψ \land χ)) \land θ) \to τ$
2		simpll	$⊢ ((φ \land (ψ \land χ \land η)) \land θ) \to φ$
3		simplr1	$⊢ ((φ \land (ψ \land χ \land η)) \land θ) \to ψ$
4		simplr2	$⊢ ((φ \land (ψ \land χ \land η)) \land θ) \to χ$
5	3 4	jca	$⊢ ((φ \land (ψ \land χ \land η)) \land θ) \to (ψ \land χ)$
6		simpr	$⊢ ((φ \land (ψ \land χ \land η)) \land θ) \to θ$
7	2 5 6 1	syl21anc	$⊢ ((φ \land (ψ \land χ \land η)) \land θ) \to τ$

Metamath Proof Explorer