This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem adantl5r

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

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

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