Metamath Proof Explorer

Theorem adantl3r

Description: Deduction adding 1 conjunct to antecedent. (Contributed by Alan Sare, 17-Oct-2017)

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

Step	Hyp	Ref	Expression
1		adantl3r.1	$⊢ (((φ \land ψ) \land χ) \land θ) \to τ$
2		id	$⊢ (φ \land ψ) \to (φ \land ψ)$
3	2	adantlr	$⊢ ((φ \land η) \land ψ) \to (φ \land ψ)$
4	3 1	sylanl1	$⊢ ((((φ \land η) \land ψ) \land χ) \land θ) \to τ$