Metamath Proof Explorer

Theorem adantl6r

Description: Deduction adding 1 conjunct to antecedent. (Contributed by Thierry Arnoux, 11-Feb-2018)

		Ref	Expression
	Hypothesis	adantl6r.1	$⊢ ((((((φ \land η) \land ζ) \land σ) \land ρ) \land μ) \land λ) \to κ$
	Assertion	adantl6r	$⊢ (((((((φ \land τ) \land η) \land ζ) \land σ) \land ρ) \land μ) \land λ) \to κ$

Step	Hyp	Ref	Expression
1		adantl6r.1	$⊢ ((((((φ \land η) \land ζ) \land σ) \land ρ) \land μ) \land λ) \to κ$
2	1	ex	$⊢ (((((φ \land η) \land ζ) \land σ) \land ρ) \land μ) \to (λ \to κ)$
3	2	adantl5r	$⊢ ((((((φ \land τ) \land η) \land ζ) \land σ) \land ρ) \land μ) \to (λ \to κ)$
4	3	imp	$⊢ (((((((φ \land τ) \land η) \land ζ) \land σ) \land ρ) \land μ) \land λ) \to κ$